---

Step * of Lemma comb_for_mon_nat_op_wf

λg,n,e,z. (n ⋅ e) ∈ g:IMonoid ⟶ n:ℕ ⟶ e:|g| ⟶ (↓True) ⟶ |g|
BY
{ ProveOpCombTyping `mon_nat_op_wf` }

---

Latex:

---

Latex:
\mlambda{}g,n,e,z.  (n  \mcdot{}  e)  \mmember{}  g:IMonoid  {}\mrightarrow{}  n:\mBbbN{}  {}\mrightarrow{}  e:|g|  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  |g|


By

---

Latex:
ProveOpCombTyping  `mon\_nat\_op\_wf`

---

Home Index