X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Flpx_sn_lpx_sn.ma;h=fe4b2b8450fe7ed8ab9499752f0bac09e645c78e;hb=37e1b4f314ffae815beca71300688040f8da6939;hp=70b8931f0a767766d495d15d9be9ac820d9f2248;hpb=c60524dec7ace912c416a90d6b926bee8553250b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma
index 70b8931f0..fe4b2b845 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma
@@ -35,11 +35,11 @@ qed-.
 
 theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 →
                      confluent2 … (lpx_sn R1) (lpx_sn R2).
-#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH *
-[ #_ #X1 #H1 #X2 #H2 -n
+#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #x #IH *
+[ #_ #X1 #H1 #X2 #H2 -x
   >(lpx_sn_inv_atom1 … H1) -X1
   >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3 by lpx_sn_atom, ex2_intro/
-| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
+| #L0 #I #V0 #Hx #X1 #H1 #X2 #H2 destruct
   elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
   elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
   elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2