X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_aaa.ma;h=b5835bef96e14770224f3a34e631a07fcb6fbd2d;hb=874cacec64d0aab52ab1a21aad23208f52f50caf;hp=f492c019b6833dbda1494c93cf066684a2c41cca;hpb=583c59b229ba770c9694c703b381542ff2e67f4e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
index f492c019b..b5835bef9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
@@ -21,7 +21,7 @@ include "basic_2/dynamic/snv.ma".
 
 (* Forward lemmas on atomic arity assignment for terms **********************)
 
-lemma snv_fwd_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A.
+lemma snv_fwd_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → ∃A. L ⊢ T ⁝ A.
 #h #g #L #T #H elim H -L -T
 [ /2 width=2/
 | #I #L #K #V #i #HLK #_ * /3 width=6/
@@ -36,6 +36,6 @@ lemma snv_fwd_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A.
 ]
 qed-.
 
-lemma snv_fwd_csn: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → L ⊢ ⬊* T.
+lemma snv_fwd_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → L ⊢ ⬊* T.
 #h #g #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/
 qed-.