X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fequivalence%2Fscpes_aaa.ma;h=761ead9be8e94018d2ef4932fb8835eae98af1b2;hb=c60524dec7ace912c416a90d6b926bee8553250b;hp=39bc00547d8cdf25fcf5f30340735106f140a0f2;hpb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma
index 39bc00547..761ead9be 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma
@@ -19,10 +19,10 @@ include "basic_2/equivalence/scpes.ma".
 
 (* Main inversion lemmas about atomic arity assignment on terms *************)
 
-theorem scpes_aaa_mono: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
+theorem scpes_aaa_mono: ∀h,g,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, d1, d2] T2 →
                         ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
                         A1 = A2.
-#h #g #G #L #T1 #T2 #l1 #l2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2
+#h #g #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2
 lapply (scpds_aaa_conf … HA1 … HT1) -T1 #HA1
 lapply (scpds_aaa_conf … HA2 … HT2) -T2 #HA2
 lapply (aaa_mono … HA1 … HA2) -L -T //