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`` 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