X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Freducibility%2Fcnf.ma;h=39ac692cda6d0b0a09239d36598d4d443def5a34;hb=44c1079dabf1d3c0b69d0155ddbaea8627ec901c;hp=50ff046038f7e1cfbc6894d15d2fcaf1f56ae047;hpb=b5db76fe31ab35bae0257cb6684c511bcc531e45;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 50ff04603..39ac692cd 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf.ma
@@ -30,4 +30,7 @@ lemma cnf_sort: ∀L,k. L ⊢ 𝐍[⋆k].
 >(cpr_inv_sort1 … H) //
 qed.
 
+axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨
+               ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → False).
+
 (* Basic_1: removed theorems 1: nf2_abst_shift *)