Step * of Lemma not_assert_elim

[b:𝔹]. ff supposing ¬↑b
BY
(Auto THEN MoveToConcl (-1) THEN BoolInd THEN Reduce THEN Auto) }


Latex:


Latex:
\mforall{}[b:\mBbbB{}].  b  =  ff  supposing  \mneg{}\muparrow{}b


By


Latex:
(Auto  THEN  MoveToConcl  (-1)  THEN  BoolInd  1  THEN  Reduce  0  THEN  Auto)




Home Index