---

Step * of Lemma testxxx_lemma

∀b:Top. (tt ∨bb ~ tt)
BY
{ ((UnivCD THENA Auto)
   THEN RW (AddrC [1] (RepeatC (UnfoldsC ``bor btrue ifthenelse``) ANDTHENC ReduceC⋅)) 0⋅
   THEN RW (AddrC [2] (UnfoldC `btrue`⋅⋅)) 0⋅
   THEN SqEqCD) }

---

Latex:

---

Latex:
\mforall{}b:Top.  (tt  \mvee{}\msubb{}b  \msim{}  tt)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RW  (AddrC  [1]  (RepeatC  (UnfoldsC  ``bor  btrue  ifthenelse``)  ANDTHENC  ReduceC\mcdot{}))  0\mcdot{}
  THEN  RW  (AddrC  [2]  (UnfoldC  `btrue`\mcdot{}\mcdot{}))  0\mcdot{}
  THEN  SqEqCD)

---

Home Index