X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fdynamic%2Fsnv.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fdynamic%2Fsnv.ma;h=2a234c2267ce4ff63fcead7177798e8e9966cd17;hb=f7386d0b74f935f07ede4be46d0489a233d68b85;hp=223dba7eecfa272c96cf493864f547cec850eecf;hpb=1f1ea7bb9e6c34626bcabd4c0142fcde98bcbbe5;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma
index 223dba7ee..2a234c226 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma
@@ -24,7 +24,7 @@ inductive snv (h:sh) (g:sd h): lenv → predicate term ≝
 | snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T)
 | snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T →
             ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 →
-            ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
+            ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
 | snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T →
             ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ W ⬌* U → snv h g L (ⓝW.T)
 .
@@ -67,7 +67,7 @@ lemma snv_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊩ ⓑ{a,I}V.T :[g] →
 fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T →
                        ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
                                    ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
-                                   ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U.
+                                   ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U.
 #h #g #L #X * -L -X
 [ #L #k #V #T #H destruct
 | #I #L #K #V0 #i #_ #_ #V #T #H destruct
@@ -80,7 +80,7 @@ qed.
 lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] →
                     ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
                                 ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
-                                ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U.
+                                ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U.
 /2 width=3/ qed-.
 
 fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T →