- new extendedd beta-reductum involving native type annotation

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / snv_aaa.ma

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 b5835bef96e14770224f3a34e631a07fcb6fbd2d..47a2b015ce53a398c684d5ae323aeff155a59592 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
@@ -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] → ⦃h, L⦄ ⊢ ⬊*[g] T.
 #h #g #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/
 qed-.