---

Step * of Lemma assert_of_bor

∀p:𝔹. ∀[q:𝔹]. uiff(↑(p ∨bq);(↑p) ∨ (↑q))
BY
{ ((D 0 THENA Auto) THEN BoolInd 1 THEN Reduce 0 THEN Auto THEN D -1 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}p:\mBbbB{}.  \mforall{}[q:\mBbbB{}].  uiff(\muparrow{}(p  \mvee{}\msubb{}q);(\muparrow{}p)  \mvee{}  (\muparrow{}q))


By

---

Latex:
((D  0  THENA  Auto)  THEN  BoolInd  1  THEN  Reduce  0  THEN  Auto  THEN  D  -1  THEN  Auto)

---

Home Index