---

Step * of Lemma generic_wf

∀[T:Type]. ∀[S:(ℕ ⟶ T) ⟶ ℙ'].  (Generic{f:ℕ⟶T|S[f]} ∈ ℙ')
BY
{ (Unfold `generic` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[S:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}'].    (Generic\{f:\mBbbN{}{}\mrightarrow{}T|S[f]\}  \mmember{}  \mBbbP{}')


By

---

Latex:
(Unfold  `generic`  0  THEN  Auto)

---

Home Index