---

Step * of Lemma RankEx1_List-list_wf

∀[T:Type]. ∀[v:RankEx1(T)].  RankEx1_List-list(v) ∈ RankEx1(T) List supposing ↑RankEx1_List?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:


\mforall{}[T:Type].  \mforall{}[v:RankEx1(T)].    RankEx1\_List-list(v)  \mmember{}  RankEx1(T)  List  supposing  \muparrow{}RankEx1\_List?(v)


By

DepprodCoDatatypeSelectorWf

---

Home Index