- predefined_virtuals: some additions

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / dynamic / nta_lift.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
index 294c1710e8ea4388d279ac1acc50ee0926beadb7..0631ca4f2f3b59c4596f0d8b167f0dfcb1f614d1 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
@@ -77,7 +77,7 @@ lemma nta_inv_bind1: ∀h,I,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{I}Y.X : U →
 elim (ntaa_inv_bind1 … (nta_ntaa … H)) -H /3 width=3 by ntaa_nta, ex3_2_intro/
 qed-.
 
-fact nta_inv_cast1_aux: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â\88\80X,Y. T = â\93£Y.X →
+fact nta_inv_cast1_aux: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â\88\80X,Y. T = â\93\9dY.X →
                      ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
 #h #L #T #U #H elim H -L -T -U
 [ #L #k #X #Y #H destruct
@@ -94,7 +94,7 @@ fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X
 qed.
 
 (* Basic_1: was: ty3_gen_cast *)
-lemma nta_inv_cast1: â\88\80h,L,X,Y,U. â¦\83h, Lâ¦\84 â\8a¢ â\93£Y.X : U →  ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
+lemma nta_inv_cast1: â\88\80h,L,X,Y,U. â¦\83h, Lâ¦\84 â\8a¢ â\93\9dY.X : U →  ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
 /2 width=3/ qed-.
 
 (* Advanced forvard lemmas **************************************************)