Step
*
of Lemma
isaxiom-bool-if-bunion-unit-prod
∀[t:Unit ⋃ (Top × Top)]. (isaxiom(t) ∈ 𝔹)
BY
{ Auto }
Latex:
Latex:
\mforall{}[t:Unit  \mcup{}  (Top  \mtimes{}  Top)].  (isaxiom(t)  \mmember{}  \mBbbB{})
By
Latex:
Auto
Home
Index