---

Step * of Lemma find_wf

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[as:T List]. ∀[d:T].  ((first a ∈ as s.t. P[a] else d) ∈ T)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[as:T  List].  \mforall{}[d:T].    ((first  a  \mmember{}  as  s.t.  P[a]  else  d)  \mmember{}  T)


By

---

Latex:
ProveWfLemma

---

Home Index