---

Step * of Lemma comb_for_mon_reduce_wf

λg,as,z. (Π as) ∈ g:IMonoid ⟶ as:(|g| List) ⟶ (↓True) ⟶ |g|
BY
{ (ProveOpCombinatorTyping Auto) `mon_reduce_wf` }

---

Latex:

---

Latex:
\mlambda{}g,as,z.  (\mPi{}  as)  \mmember{}  g:IMonoid  {}\mrightarrow{}  as:(|g|  List)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  |g|


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `mon\_reduce\_wf`

---

Home Index