- predefined_virtuals: some additions

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / static / sta.ma

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 4c38a083b50d3ebb4a3ad49c8a4391a351e39ff1..20302c623c9be9ac68662cced346494be14ac3eb 100644 (file)
--- 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: â\88\80L,W,T,U. sta h L T U â\86\92 sta h L (â\93£W. T) U
+| sta_cast: â\88\80L,W,T,U. sta h L T U â\86\92 sta h L (â\93\9dW. 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: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T â\80¢ U â\86\92 â\88\80X,Y. T = â\93£Y.X →
+fact sta_inv_cast1_aux: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T â\80¢ U â\86\92 â\88\80X,Y. T = â\93\9dY.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: â\88\80h,L,X,Y,U. â¦\83h, Lâ¦\84 â\8a¢ â\93£Y.X • U →  ⦃h, L⦄ ⊢ X • U.
+lemma sta_inv_cast1: â\88\80h,L,X,Y,U. â¦\83h, Lâ¦\84 â\8a¢ â\93\9dY.X • U →  ⦃h, L⦄ ⊢ X • U.
 /2 width=4/ qed-.