---

Step * of Lemma mk-coset_wf

∀[T:Type]. ∀[f:T ⟶ coSet{i:l}].  (mk-coset(T;f) ∈ coSet{i:l})
BY
{ (Auto THEN coSetD 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  coSet\{i:l\}].    (mk-coset(T;f)  \mmember{}  coSet\{i:l\})


By

---

Latex:
(Auto  THEN  coSetD  0  THEN  ProveWfLemma)

---

Home Index