---

Step * of Lemma comb_for_mon_itop_wf

λg,p,q,E,z. (Π p ≤ i < q. E[i]) ∈ g:IMonoid ⟶ p:ℤ ⟶ q:ℤ ⟶ E:({p..q-} ⟶ |g|) ⟶ (↓True) ⟶ |g|
BY
{ ProveOpCombTyping `mon_itop_wf` }

---

Latex:

---

Latex:
\mlambda{}g,p,q,E,z.  (\mPi{}  p  \mleq{}  i  <  q.  E[i])  \mmember{}  g:IMonoid  {}\mrightarrow{}  p:\mBbbZ{}  {}\mrightarrow{}  q:\mBbbZ{}  {}\mrightarrow{}  E:(\{p..q\msupminus{}\}  {}\mrightarrow{}  |g|)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  |g|


By

---

Latex:
ProveOpCombTyping  `mon\_itop\_wf`

---

Home Index