---

Step * of Lemma list-monad_wf

ListMonad ∈ Monad
BY
{ (ProveWfLemma THEN All Reduce THEN Auto) }

1
1. T : Type
2. m : T List
⊢ concat(map(λx.[x];m)) = m ∈ (T List)

---

Latex:

---

Latex:
ListMonad  \mmember{}  Monad


By

---

Latex:
(ProveWfLemma  THEN  All  Reduce  THEN  Auto)

---

Home Index