---

Step * of Lemma comb_for_mon_when_wf

λg,b,p,z. (when b. p) ∈ g:IMonoid ⟶ b:𝔹 ⟶ p:|g| ⟶ (↓True) ⟶ |g|
BY
{ ProveOpCombTyping `mon_when_wf` }

---

Latex:

---

Latex:
\mlambda{}g,b,p,z.  (when  b.  p)  \mmember{}  g:IMonoid  {}\mrightarrow{}  b:\mBbbB{}  {}\mrightarrow{}  p:|g|  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  |g|


By

---

Latex:
ProveOpCombTyping  `mon\_when\_wf`

---

Home Index