---

Step * 1 1 of Lemma assert_of_eq_bool


1. p : 𝔹
2. q : 𝔹
⊢ uiff(↑((p ∧b q) ∨b((¬bp) ∧b (¬bq)));p = q)
BY
{ ((BoolCases 2 THEN Auto) THEN BoolCases 1 THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \mBbbB{}
2.  q  :  \mBbbB{}
\mvdash{}  uiff(\muparrow{}((p  \mwedge{}\msubb{}  q)  \mvee{}\msubb{}((\mneg{}\msubb{}p)  \mwedge{}\msubb{}  (\mneg{}\msubb{}q)));p  =  q)


By

---

Latex:
((BoolCases  2  THEN  Auto)  THEN  BoolCases  1  THEN  Auto)

---

Home Index