X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcpr_lift.ma;h=b384ad2df1be01f27f07f49e82a8b7ce4c128c8b;hb=fdb2c62b58006b82c015ba70b494d50c7860e28f;hp=6d626e91d9df88c773e2f0ce2d1100803048b4a0;hpb=4aa431513ffa0ce0accf81e6e9ea4b9314d468e3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
index 6d626e91d..b384ad2df 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
@@ -96,7 +96,7 @@ lemma cpr_inv_lift1: ∀G. l_deliftable_sn (cpr G).
   elim (IHV12 … HLK … HV01) -V1 #V3 #HV32 #HV03
   elim (IHT12 (K.ⓛW0) … HT01) -T1 /2 width=1/ #T3 #HT32 #HT03
   elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
-  @ex2_intro [2: /3 width=2/ | skip |3: /2 width=1/ ] (**) (* /4 width=6/ is slow *) 
+  @ex2_intro [2: /3 width=2/ | skip |3: /2 width=1/ ] (**) (* /4 width=6/ is slow *)
 | #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #d #e #HLK #X #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct