---

Step * of Lemma comb_for_int_seg_wf

λm,n,z. {m..n-} ∈ m:ℤ ⟶ n:ℤ ⟶ (↓True) ⟶ 𝕌1
BY
{ (ProveOpCombinatorTyping Auto) `int_seg_wf` }

---

Latex:

---

Latex:
\mlambda{}m,n,z.  \{m..n\msupminus{}\}  \mmember{}  m:\mBbbZ{}  {}\mrightarrow{}  n:\mBbbZ{}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbU{}\msubone{}


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `int\_seg\_wf`

---

Home Index