Step
*
of Lemma
equal-bnot
∀[x,y:𝔹]. uiff(x = ¬by;¬x = y)
BY
{ ((UnivCD THENA Auto)
THEN AutoBoolCase ⌜y⌝⋅
THEN (RWO "eqtt_to_assert" 0 THENA Auto)
THEN (RWO "eqff_to_assert" 0 THENA Auto)
THEN (RW assert_pushdownC 0 THENA Auto)
THEN Auto) }
1
1. x : 𝔹
2. y : 𝔹
3. ¬↑y
4. ¬¬↑x
⊢ ↑x
Latex:
Latex:
\mforall{}[x,y:\mBbbB{}]. uiff(x = \mneg{}\msubb{}y;\mneg{}x = y)
By
Latex:
((UnivCD THENA Auto)
THEN AutoBoolCase \mkleeneopen{}y\mkleeneclose{}\mcdot{}
THEN (RWO "eqtt\_to\_assert" 0 THENA Auto)
THEN (RWO "eqff\_to\_assert" 0 THENA Auto)
THEN (RW assert\_pushdownC 0 THENA Auto)
THEN Auto)
Home
Index