X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fcomputation%2Fcsx_lift.ma;h=fc3b016e674cac6f09baf63a3bce845f89f9ece0;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=6bda54375d5d7e62c169cb041947668ca2661bba;hpb=d2545ffd201b1aa49887313791386add78fa8603;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/csx_lift.ma
index 6bda54375..fc3b016e6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/computation/csx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/csx_lift.ma
@@ -27,7 +27,7 @@ lemma csx_lift: ∀h,g,G,L2,L1,T1,s,l,m. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 →
 @csx_intro #T #HLT2 #HT2
 elim (cpx_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10
 @(IHT1 … HLT10) // -L1 -L2 #H destruct
->(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1 by/
+>(lift_mono … HT0 … HT12) in HT2; -T0 /2 width=1 by/
 qed.
 
 (* Basic_1: was just: sn3_gen_lift *)
@@ -38,7 +38,7 @@ lemma csx_inv_lift: ∀h,g,G,L2,L1,T1,s,l,m. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 →
 elim (lift_total T l m) #T0 #HT0
 lapply (cpx_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10
 @(IHT1 … HLT10) // -L1 -L2 #H destruct
->(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1 by/
+>(lift_inj … HT0 … HT21) in HT2; -T0 /2 width=1 by/
 qed.
 
 (* Advanced inversion lemmas ************************************************)