---

Step * of Lemma bexists_wf

∀A:Type. ∀as:A List. ∀f:A ⟶ 𝔹.  (∃bx(:A) ∈ as. f[x] ∈ 𝔹)
BY
{ ((Auto THEN Unfold `bexists` 0) THEN MemCD THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}as:A  List.  \mforall{}f:A  {}\mrightarrow{}  \mBbbB{}.    (\mexists{}\msubb{}x(:A)  \mmember{}  as.  f[x]  \mmember{}  \mBbbB{})


By

---

Latex:
((Auto  THEN  Unfold  `bexists`  0)  THEN  MemCD  THEN  Try  (Complete  (Auto)))

---

Home Index