Step
*
of Lemma
eqff_to_assert
∀[b:𝔹]. uiff(b = ff;↑¬
b
b)
BY
{ (D 0 THENA Auto) }
1
1. b : 𝔹
⊢ uiff(b = ff;↑¬
b
b)
Latex:
Latex:
\mforall{}[b:\mBbbB{}]. uiff(b = ff;\muparrow{}\mneg{}\msubb{}b)
By
Latex:
(D 0 THENA Auto)
Home
Index