X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Fcnf.ma;h=41f3633683347b3504b203173ea22cc4d6c71129;hb=5ac2dc4e01aca542ddd13c02b304c646d8df9799;hp=1156dcf68ff65ab85267a715e1e126f4154dd227;hpb=a386e0eb6b20909ae78c825203d77647b8fde30c;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
index 1156dcf68..41f363368 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
@@ -25,13 +25,13 @@ interpretation
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: nf2_sort *)
-lemma cnf_sort: ∀L,k. L ⊢ 𝐍[⋆k].
+lemma cnf_sort: ∀L,k. L ⊢ 𝐍⦃⋆k⦄.
 #L #k #X #H
 >(cpr_inv_sort1 … H) //
 qed.
 
 (* Basic_1: was: nf2_dec *)
-axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨
+axiom cnf_dec: ∀L,T1. L ⊢ 𝐍⦃T1⦄ ∨
                ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥).
 
 (* Basic_1: removed theorems 1: nf2_abst_shift *)