---

Step * of Lemma eqff_assert_2

∀[b:Decision]. uiff(b = ff ∈ Decision;¬↑b)
BY
{ (With ⌜Decision⌝ (D 0)⋅
   THEN Try (DVar `b')
   THEN RepUR ``decision assert bfalse`` 0
   THEN Auto
   THEN Try ((SimpHyp (-1)))) }

---

Latex:

---

Latex:
\mforall{}[b:Decision].  uiff(b  =  ff;\mneg{}\muparrow{}b)


By

---

Latex:
(With  \mkleeneopen{}Decision\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Try  (DVar  `b')
  THEN  RepUR  ``decision  assert  bfalse``  0
  THEN  Auto
  THEN  Try  ((SimpHyp  (-1))))

---

Home Index