Finalized copy sub-machine of the universal turing machine. Some new results

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
index f0bf7119e8dee22fa8e8bb694096f4e8b82a328c..b36725d92ffc54a1c24c275c5bb21730304db7ab 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
@@ -52,7 +52,7 @@ qed-.
 (* Advanced properties ******************************************************)
 
 lemma nta_cast_alt: ∀h,L,T,W,U. ⦃h, L⦄ ⊢ T : W → ⦃h, L⦄ ⊢ T : U →
-             â¦\83h, Lâ¦\84 â\8a¢ â\93£W.T : U.
+             â¦\83h, Lâ¦\84 â\8a¢ â\93\9dW.T : U.
 #h #L #T #W #U #HTW #HTU
 lapply (nta_mono … HTW … HTU) #HWU
 elim (nta_fwd_correct … HTU) -HTU /3 width=3/