---

Step * of Lemma ring-as-list_wf

∀[T:Type]. ∀[L:T List]. ∀[f:{i:T| (i ∈ L)}  ⟶ {i:T| (i ∈ L)} ].  (ring-as-list(T;L;f) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[f:\{i:T|  (i  \mmember{}  L)\}    {}\mrightarrow{}  \{i:T|  (i  \mmember{}  L)\}  ].    (ring-as-list(T;L;f)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index