Step * of Lemma bnot-tt

[a:𝔹]. ff supposing ¬btt
BY
((D THENA Auto) THEN AutoBoolCase ⌜a⌝⋅}


Latex:


Latex:
\mforall{}[a:\mBbbB{}].  a  \msim{}  ff  supposing  \mneg{}\msubb{}a  \msim{}  tt


By


Latex:
((D  0  THENA  Auto)  THEN  AutoBoolCase  \mkleeneopen{}a\mkleeneclose{}\mcdot{})




Home Index