X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flift.ma;h=f90b349b3de0b7fe55dc57e698833d5f666ce3dc;hb=c69a33bba2ae2f37953737940fb45149136cf054;hp=e48d22e20477b0b796a3f26d6a64d13df42bc563;hpb=65008df95049eb835941ffea1aa682c9253c4c2b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
index e48d22e20..f90b349b3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
@@ -21,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))
@@ -274,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 →
@@ -282,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}.