Step
*
of Lemma
has-value-bnot
∀[a:Base]. (a)↓ supposing (¬ba)↓
BY
{ (Auto THEN RepUR ``bnot ifthenelse`` (-1) THEN HasValueD (-1) THEN Auto) }
Latex:
Latex:
\mforall{}[a:Base]. (a)\mdownarrow{} supposing (\mneg{}\msubb{}a)\mdownarrow{}
By
Latex:
(Auto THEN RepUR ``bnot ifthenelse`` (-1) THEN HasValueD (-1) THEN Auto)
Home
Index