---

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