Step
*
of Lemma
not_functionality_wrt_uimplies
∀[P,Q:ℙ]. ({P supposing Q}
⇒ {¬Q supposing ¬P})
BY
{ (Unfolds ``not guard`` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[P,Q:\mBbbP{}]. (\{P supposing Q\} {}\mRightarrow{} \{\mneg{}Q supposing \mneg{}P\})
By
Latex:
(Unfolds ``not guard`` 0 THEN Auto)
Home
Index