---

Step * of Lemma comb_for_nat_op_wf

λg,n,e,z. n x(*;e) e ∈ g:IMonoid ⟶ n:ℕ ⟶ e:|g| ⟶ (↓True) ⟶ |g|
BY
{ ProveOpCombTyping `nat_op_wf` }

---

Latex:

---

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


By

---

Latex:
ProveOpCombTyping  `nat\_op\_wf`

---

Home Index