update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / csx_cnx_vector.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
index 6110714a1d11908f9ac99f03d24ceb29077ff142..ec1957501be9a8b51ef19bc5011b6df4d923ec96 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
@@ -24,8 +24,8 @@ include "basic_2/rt_computation/csx_vector.ma".
 
 (* Basic_1: was just: sn3_appls_lref *)
 lemma csx_applv_cnx (G) (L):
-      â\88\80T. ð\9d\90\92â\9dªTâ\9d« â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈𝐍 T →
-      â\88\80Vs. â\9dªG,Lâ\9d« â\8a¢ â¬\88*ð\9d\90\92 Vs â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈*𝐒 ⒶVs.T.
+      â\88\80T. ð\9d\90\92â\9d¨Tâ\9d© â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈𝐍 T →
+      â\88\80Vs. â\9d¨G,Lâ\9d© â\8a¢ â¬\88*ð\9d\90\92 Vs â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈*𝐒 ⒶVs.T.
 #G #L #T #H1T #H2T #Vs elim Vs -Vs
 [ #_ normalize in ⊢ (???%); /2 width=1 by cnx_csx/
 | #V #Vs #IHV #H
@@ -41,5 +41,5 @@ qed.
 
 (* Note: strong normalization does not depend on this any more *)
 lemma csx_applv_sort (G) (L):
-      â\88\80s,Vs. â\9dªG,Lâ\9d« â\8a¢ â¬\88*ð\9d\90\92 Vs â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈*𝐒 ⒶVs.⋆s.
+      â\88\80s,Vs. â\9d¨G,Lâ\9d© â\8a¢ â¬\88*ð\9d\90\92 Vs â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈*𝐒 ⒶVs.⋆s.
 /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ qed.