- some renaming according to the written version of basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / equivalence / scpes_aaa.ma

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 39bc00547d8cdf25fcf5f30340735106f140a0f2..761ead9be8e94018d2ef4932fb8835eae98af1b2 100644 (file)
--- 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 //