---

Step * of Lemma bl-exists-cons

∀[f,u,v:Top].  ((∃x∈[u / v].f[x])_b ~ f[u] ∨b(∃x∈v.f[x])_b)
BY
{ (RepUR ``bl-exists`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f,u,v:Top].    ((\mexists{}x\mmember{}[u  /  v].f[x])\_b  \msim{}  f[u]  \mvee{}\msubb{}(\mexists{}x\mmember{}v.f[x])\_b)


By

---

Latex:
(RepUR  ``bl-exists``  0  THEN  Auto)

---

Home Index