---

Step * of Lemma coWsup_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[a:A]. ∀[f:B[a] ⟶ coW(A;a.B[a])].  (coWsup(a;f) ∈ coW(A;a.B[a]))
BY
{ (Auto THEN coWD 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[a:A].  \mforall{}[f:B[a]  {}\mrightarrow{}  coW(A;a.B[a])].    (coWsup(a;f)  \mmember{}  coW(A;a.B[a]))


By

---

Latex:
(Auto  THEN  coWD  0  THEN  ProveWfLemma)

---

Home Index