(* 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
]
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].
/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
]
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-.