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=fdb2c62b58006b82c015ba70b494d50c7860e28f;hp=ba117d867f12573db855baa9ca910921ae324bd8;hpb=4aa431513ffa0ce0accf81e6e9ea4b9314d468e3;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 ba117d867..f90b349b3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
@@ -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}.