X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fstatic%2Fsta.ma;h=20302c623c9be9ac68662cced346494be14ac3eb;hb=bcdba61431ead40a18a6ac04285cd6513d491287;hp=4c38a083b50d3ebb4a3ad49c8a4391a351e39ff1;hpb=913512bbc9202f2109d53acd43dc8c0270b17184;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma
index 4c38a083b..20302c623 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma
@@ -27,7 +27,7 @@ inductive sta (h:sh): lenv → relation term ≝
             sta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
 | sta_appl: ∀L,V,T,U. sta h L T U →
             sta h L (ⓐV.T) (ⓐV.U)
-| sta_cast: ∀L,W,T,U. sta h L T U → sta h L (ⓣW. T) U
+| sta_cast: ∀L,W,T,U. sta h L T U → sta h L (ⓝW. T) U
 .
 
 interpretation "static type assignment (term)"
@@ -111,7 +111,7 @@ lemma sta_inv_appl1: ∀h,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X • U →
                      ∃∃Z. ⦃h, L⦄ ⊢ X • Z & U = ⓐY.Z.
 /2 width=3/ qed-.
 
-fact sta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓣY.X →
+fact sta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓝY.X →
                      ⦃h, L⦄ ⊢ X • U.
 #h #L #T #U * -L -T -U
 [ #L #k #X #Y #H destruct
@@ -124,5 +124,5 @@ fact sta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓣY.
 qed.
 
 (* Basic_1: was: sty0_gen_cast *)
-lemma sta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X • U →  ⦃h, L⦄ ⊢ X • U.
+lemma sta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓝY.X • U →  ⦃h, L⦄ ⊢ X • U.
 /2 width=4/ qed-.