X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fequivalence%2Fscpes_aaa.ma;h=f42ebdbc91f776095984d3a10d6a7ad568aab55a;hb=e62715437a9c39244c9809c00585a5ef44a39797;hp=39bc00547d8cdf25fcf5f30340735106f140a0f2;hpb=5902d6da146ca78b0ed5d062e3968f52868147c5;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..f42ebdbc9 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,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, 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 #o #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 //