---

Step * of Lemma comb_for_lt_int_wf

λi,j,z. i <z j ∈ i:ℤ ⟶ j:ℤ ⟶ (↓True) ⟶ 𝔹
BY
{ (ProveOpCombinatorTyping Auto) `lt_int_wf` }

---

Latex:

---

Latex:
\mlambda{}i,j,z.  i  <z  j  \mmember{}  i:\mBbbZ{}  {}\mrightarrow{}  j:\mBbbZ{}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbB{}


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `lt\_int\_wf`

---

Home Index