---

Step * of Lemma for_wf

∀[A,B,C:Type]. ∀[f:B ⟶ C ⟶ C]. ∀[k:C]. ∀[as:A List]. ∀[g:A ⟶ B].  (For{A,f,k} x ∈ as. g[x] ∈ C)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[f:B  {}\mrightarrow{}  C  {}\mrightarrow{}  C].  \mforall{}[k:C].  \mforall{}[as:A  List].  \mforall{}[g:A  {}\mrightarrow{}  B].    (For\{A,f,k\}  x  \mmember{}  as.  g[x]  \mmember{}  C)


By

---

Latex:
ProveWfLemma

---

Home Index