- predefined_virtuals: some additions

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
index 481683f2ab80f237478886669870f30739bca6d6..c9b39fce3de056f130ef5ed939a0f627f2a54a50 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
@@ -55,7 +55,7 @@ elim (term_eq_dec T1 T2) #HT12
 qed.
 
 (* Basic_1: was: sn3_cast *)
-lemma csn_cast: â\88\80L,W. L â\8a¢ â¬\87* W â\86\92 â\88\80T. L â\8a¢ â¬\87* T â\86\92 L â\8a¢ â¬\87* â\93£W. T.
+lemma csn_cast: â\88\80L,W. L â\8a¢ â¬\87* W â\86\92 â\88\80T. L â\8a¢ â¬\87* T â\86\92 L â\8a¢ â¬\87* â\93\9dW. T.
 #L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
 @csn_intro #X #H1 #H2
 elim (cpr_inv_cast1 … H1) -H1