X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Fllpx_sn_alt_rec.ma;h=6cd1b9bd97416a5507452dd157e81af80819545e;hb=37e1b4f314ffae815beca71300688040f8da6939;hp=0f38faaa8a8b6f3c9f285c2dd5489a4f31483e0e;hpb=c60524dec7ace912c416a90d6b926bee8553250b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma
index 0f38faaa8..6cd1b9bd9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma
@@ -195,17 +195,17 @@ qed.
 (* Main inversion lemmas ****************************************************)
 
 theorem llpx_sn_alt_r_inv_lpx_sn: ∀R,T,L1,L2,l. llpx_sn_alt_r R l T L1 L2 → llpx_sn R l T L1 L2.
-#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #n #IH #L1 * *
+#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #x #IH #L1 * *
 [1,3: /3 width=4 by llpx_sn_alt_r_fwd_length, llpx_sn_gref, llpx_sn_sort/
-| #i #Hn #L2 #l #H lapply (llpx_sn_alt_r_fwd_length … H)
+| #i #Hx #L2 #l #H lapply (llpx_sn_alt_r_fwd_length … H)
   #HL12 elim (llpx_sn_alt_r_fwd_lref … H) -H
   [ * /2 width=1 by llpx_sn_free/
   | /2 width=1 by llpx_sn_skip/
   | * /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
   ]
-| #a #I #V #T #Hn #L2 #l #H elim (llpx_sn_alt_r_inv_bind … H) -H
+| #a #I #V #T #Hx #L2 #l #H elim (llpx_sn_alt_r_inv_bind … H) -H
   /3 width=1 by llpx_sn_bind/
-| #I #V #T #Hn #L2 #l #H elim (llpx_sn_alt_r_inv_flat … H) -H
+| #I #V #T #Hx #L2 #l #H elim (llpx_sn_alt_r_inv_flat … H) -H
   /3 width=1 by llpx_sn_flat/
 ]
 qed-.