---

Step * of Lemma mem_f_wf

∀T:Type. ∀a:T. ∀bs:T List.  (mem_f(T;a;bs) ∈ ℙ)
BY
{ (InductionOnList THEN RecCaseSplit `mem_f` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}a:T.  \mforall{}bs:T  List.    (mem\_f(T;a;bs)  \mmember{}  \mBbbP{})


By

---

Latex:
(InductionOnList  THEN  RecCaseSplit  `mem\_f`  THEN  Auto)

---

Home Index