(* *)
(**************************************************************************)
+include "basic_2/notation/relations/rlift_4.ma".
include "basic_2/grammar/term_weight.ma".
include "basic_2/grammar/term_simple.ma".
(* Basic_1: includes:
lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
*)
-inductive lift: nat → nat → relation term ≝
+inductive lift: relation4 nat nat term term ≝
| lift_sort : ∀k,d,e. lift d e (⋆k) (⋆k)
| lift_lref_lt: ∀i,d,e. i < d → lift d e (#i) (#i)
| lift_lref_ge: ∀i,d,e. d ≤ i → lift d e (#i) (#(i + e))
* [ #a ] #I #T2 #V1 #U1 #d #e #H
[ elim (lift_inv_bind1 … H) -H /2 width=4/
| elim (lift_inv_flat1 … H) -H /2 width=4/
-]
+]
qed-.
lemma lift_fwd_pair2: ∀I,T1,V2,U2,d,e. ⇧[d,e] T1 ≡ ②{I}V2.U2 →
* [ #a ] #I #T1 #V2 #U2 #d #e #H
[ elim (lift_inv_bind2 … H) -H /2 width=4/
| elim (lift_inv_flat2 … H) -H /2 width=4/
-]
+]
qed-.
lemma lift_fwd_tw: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}.