Progress.

[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 00647e43ce09636f76efdb0e9f4c7c883644840f..1156dcf68ff65ab85267a715e1e126f4154dd227 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
@@ -32,6 +32,6 @@ qed.
 
 (* Basic_1: was: nf2_dec *)
 axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨
-               ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → False).
+               ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥).
 
 (* Basic_1: removed theorems 1: nf2_abst_shift *)