X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcpe.ma;h=8877fa44f2213d357e193aef2b74f17e2b606f48;hb=cb38da6095e3af84131a3ebf47a9f252f34a804c;hp=22d7ea92a49c5e61b739a489d36045197cce0e36;hpb=e0827239f4b44f2af9c7f88c4c7c41f2a193ae37;p=helm.git

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 22d7ea92a..8877fa44f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma
@@ -18,7 +18,7 @@ include "basic_2/computation/csn.ma".
 (* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
 
 definition cpe: lenv → relation term ≝
-                λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍[T2].
+                λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍⦃T2⦄.
 
 interpretation "context-sensitive parallel evaluation (term)"
    'PEval L T1 T2 = (cpe L T1 T2).
@@ -26,7 +26,7 @@ interpretation "context-sensitive parallel evaluation (term)"
 (* Basic_properties *********************************************************)
 
 (* Basic_1: was: nf2_sn3 *)
-lemma cpe_csn: ∀L,T1. L ⊢ ⬇* T1 → ∃T2. L ⊢ T1 ➡* 𝐍[T2].
+lemma cpe_csn: ∀L,T1. L ⊢ ⬇* T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄.
 #L #T1 #H @(csn_ind … H) -T1
 #T1 #_ #IHT1
 elim (cnf_dec L T1) /3 width=3/