---

Step * of Lemma comb_for_int_op_wf

λg,a,e,z. a x(*;e;~) e ∈ g:Group{i} ⟶ a:ℤ ⟶ e:|g| ⟶ (↓True) ⟶ |g|
BY
{ ProveOpCombTyping `int_op_wf` }

---

Latex:

---

Latex:
\mlambda{}g,a,e,z.  a  x(*;e;\msim{})  e  \mmember{}  g:Group\{i\}  {}\mrightarrow{}  a:\mBbbZ{}  {}\mrightarrow{}  e:|g|  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  |g|


By

---

Latex:
ProveOpCombTyping  `int\_op\_wf`

---

Home Index