- we introduced the pointer_step rc in the perspective of proving

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma
index 8877fa44f2213d357e193aef2b74f17e2b606f48..285e6e4fc23c18d04878e2323a1d0b8009c70a0c 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma
@@ -26,7 +26,7 @@ interpretation "context-sensitive parallel evaluation (term)"
 (* Basic_properties *********************************************************)
 
 (* Basic_1: was: nf2_sn3 *)
-lemma cpe_csn: â\88\80L,T1. L â\8a¢ â¬\87* T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄.
+lemma cpe_csn: â\88\80L,T1. L â\8a¢ â¬\8a* T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄.
 #L #T1 #H @(csn_ind … H) -T1
 #T1 #_ #IHT1
 elim (cnf_dec L T1) /3 width=3/