- predefined_virtuals: some additions

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / csn_tstc_vector.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
index e1a64150599580ba687f254c81f3e33ce4ebe60c..205642fac210cb13bfcf95d8de7081302b716343 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
@@ -22,7 +22,7 @@ include "basic_2/computation/csn_vector.ma".
 (* Advanced properties ******************************************************)
 
 (* Basic_1: was only: sn3_appls_lref *)
-lemma csn_applv_cnf: ∀L,T. 𝐒[T] → L ⊢ 𝐍[T] → 
+lemma csn_applv_cnf: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ → 
                      ∀Vs. L ⊢ ⬇* Vs → L ⊢ ⬇* ⒶVs.T.
 #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(csn_cnf … H2T) ] (**) (* /2 width=1/ does not work *)
 #V #Vs #IHV #H
@@ -90,7 +90,7 @@ qed.
 (* Basic_1: was: sn3_appls_cast *)
 lemma csn_applv_tau: ∀L,W. L ⊢ ⬇* W →
                      ∀Vs,T. L ⊢ ⬇* ⒶVs. T →
-                     L â\8a¢ â¬\87* â\92¶Vs. â\93£W. T.
+                     L â\8a¢ â¬\87* â\92¶Vs. â\93\9dW. T.
 #L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW
 #V #Vs #IHV #T #H1T
 lapply (csn_fwd_pair_sn … H1T) #HV