update in 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 761ead9be8e94018d2ef4932fb8835eae98af1b2..f42ebdbc91f776095984d3a10d6a7ad568aab55a 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,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, d1, d2] 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 #d1 #d2 * #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 //