---

Step * of Lemma eqtt_assert_2

∀[b:Decision]. uiff(b = tt ∈ Decision;↑b)
BY
{ TACTIC:(RepUR ``decision assert btrue ifthenelse`` 0
          THEN Auto
          THEN DVar `b'
          THEN All Reduce
          THEN Auto
          THEN (SimpHyp (-1))
          THEN EqCD
          THEN Auto) }

---

Latex:

---

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


By

---

Latex:
TACTIC:(RepUR  ``decision  assert  btrue  ifthenelse``  0
                THEN  Auto
                THEN  DVar  `b'
                THEN  All  Reduce
                THEN  Auto
                THEN  (SimpHyp  (-1))
                THEN  EqCD
                THEN  Auto)

---

Home Index