manual commit

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / cnf.ma

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 39ac692cda6d0b0a09239d36598d4d443def5a34..00647e43ce09636f76efdb0e9f4c7c883644840f 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/cpr.ma".
 
 (* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
 
@@ -30,6 +30,7 @@ lemma cnf_sort: ∀L,k. L ⊢ 𝐍[⋆k].
 >(cpr_inv_sort1 … H) //
 qed.
 
+(* Basic_1: was: nf2_dec *)
 axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨
                ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → False).