- a caracterization of the top elements of the local evironment

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
index 3ae5bfd176e142ef0a505e4fa93f4e8d0e1c585d..84b64083158b5d95e520aa6ad09cfa793c7ee765 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/grammar/term_simple.ma".
+include "basic_2/grammar/term_simple.ma".
 
 (* CONTEXT-FREE REDUCIBLE TERMS *********************************************)
 
@@ -33,7 +33,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T =  ⓪{I} → False.
+fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T =  ⓪{I} → ⊥.
 #I #T * -T
 [ #V #T #_ #H destruct
 | #V #T #_ #H destruct
@@ -45,7 +45,7 @@ fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T =  ⓪{I} → False.
 ]
 qed.
 
-lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → False.
+lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → ⊥.
 /2 width=4/ qed-.
 
 fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T =  ⓛW. U → 𝐑[W] ∨ 𝐑[U].
@@ -64,7 +64,7 @@ lemma trf_inv_abst: ∀V,T. 𝐑[ⓛV.T] → 𝐑[V] ∨ 𝐑[T].
 /2 width=3/ qed-.
 
 fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T =  ⓐW. U →
-                       ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
+                       ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → ⊥).
 #W #U #T * -T
 [ #V #T #_ #H destruct
 | #V #T #_ #H destruct
@@ -77,5 +77,5 @@ fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T =  ⓐW. U →
 ]
 qed.
 
-lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
+lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → ⊥).
 /2 width=3/ qed-.