X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcpr_lift.ma;h=101e2b029da3e875cc34c73885ae6fa02976c244;hb=a76f56fdad6348b167376093920650379c9936d4;hp=dcd6307a76db899ba9c05e9e601f04f4a8ffd65a;hpb=2ba2dc23443ad764adab652e06d6f5ed10bd912d;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 dcd6307a7..101e2b029 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
@@ -61,7 +61,7 @@ qed.
 (* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
 lemma cpr_inv_lift1: ∀G. l_deliftable_sn (cpr G).
 #G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #G #L #i #K #s #d #e #_ #T1 #H
+[ * #i #G #L #K #s #d #e #_ #T1 #H
   [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
   | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
   | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/