X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftif.ma;h=653ed47002d99ce924550028f162b8504fa00e85;hb=78d4844bcccb3deb58a3179151c3045298782b18;hp=d3e01081856c9d5e12759d26d0beea710868ac6e;hpb=a8c166f1e1baeeae04553058bd179420ada8bbe7;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
index d3e010818..653ed4700 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
@@ -16,14 +16,14 @@ include "basic_2/reducibility/trf.ma".
 
 (* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************)
 
-definition tif: predicate term ≝ λT. 𝐑[T] → False.
+definition tif: predicate term ≝ λT. 𝐑[T] → ⊥.
 
 interpretation "context-free irreducibility (term)"
    'NotReducible T = (tif T).
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma tif_inv_abbr: ∀V,T. 𝐈[ⓓV.T] → False.
+lemma tif_inv_abbr: ∀V,T. 𝐈[ⓓV.T] → ⊥.
 /2 width=1/ qed-.
 
 lemma tif_inv_abst: ∀V,T. 𝐈[ⓛV.T] → 𝐈[V] ∧ 𝐈[T].
@@ -35,7 +35,7 @@ generalize in match HVT; -HVT elim T -T //
 * // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
 qed-.
 
-lemma tif_inv_cast: ∀V,T. 𝐈[ⓣV.T] → False.
+lemma tif_inv_cast: ∀V,T. 𝐈[ⓣV.T] → ⊥.
 /2 width=1/ qed-.
 
 (* Basic properties *********************************************************)