---

Step * 1 of Lemma assert_of_eq_bool


1. p : 𝔹
2. q : 𝔹
⊢ uiff(↑p =b q;p = q)
BY
{ Unfold `eq_bool` 0 }

1
1. p : 𝔹
2. q : 𝔹
⊢ uiff(↑((p ∧b q) ∨b((¬bp) ∧b (¬bq)));p = q)

---

Latex:

---

Latex:

1.  p  :  \mBbbB{}
2.  q  :  \mBbbB{}
\mvdash{}  uiff(\muparrow{}p  =b  q;p  =  q)


By

---

Latex:
Unfold  `eq\_bool`  0

---

Home Index