partial commit: just the components before "static" ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lpxs_aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma
index b05385da5f2b9313167e34eb682be4b29b47c2d2..e866102d4835ab2fe1f60ab397da6d2ccfd387c6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma
@@ -20,9 +20,9 @@ include "basic_2/computation/lpxs.ma".
 (* Properties about atomic arity assignment on terms ************************)
 
 lemma aaa_lpxs_conf: ∀h,g,L1,T,A.
-                     L1 ⊢ T ⁝ A → ∀L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → L2 ⊢ T ⁝ A.
+                     L1 ⊢ T ⁝ A → ∀L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 → L2 ⊢ T ⁝ A.
 #h #g #L1 #T #A #HT #L2 #HL12
-@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/
+@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/
 qed-.
 
 lemma aaa_lprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A.