- advances on hereditarily free variables: now "frees" is primitive

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
index e72288dffbedbcba96dec91c036aa116b11e47ca..f90b349b3de0b7fe55dc57e698833d5f666ce3dc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/notation/relations/rlift_4.ma".
 include "basic_2/grammar/term_weight.ma".
 include "basic_2/grammar/term_simple.ma".
 
@@ -20,7 +21,7 @@ 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))
@@ -273,7 +274,7 @@ lemma lift_fwd_pair1: ∀I,T2,V1,U1,d,e. ⇧[d,e] ②{I}V1.U1 ≡ T2 →
 * [ #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 →
@@ -281,7 +282,7 @@ 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}.