---

Step * of Lemma assert_of_eq_bool

∀[p,q:𝔹].  uiff(↑p =b q;p = q)
BY
{ (UnivCD THENA Auto) }

1
1. p : 𝔹
2. q : 𝔹
⊢ uiff(↑p =b q;p = q)

---

Latex:

---

Latex:
\mforall{}[p,q:\mBbbB{}].    uiff(\muparrow{}p  =b  q;p  =  q)


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index