- 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 5660846151ccccf34091579dec50f40f283ee317..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
@@ -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