---

Step * of Lemma le_witness

∀[i,j:ℤ]. ∀[x:i ≤ j].  (x = <λx.x, Ax, Ax> ∈ (i ≤ j))
BY
{ Auto }

1
1. i : ℤ
2. j : ℤ
3. x : i ≤ j
⊢ x = <λx.x, Ax, Ax> ∈ (i ≤ j)

---

Latex:

---

Latex:
\mforall{}[i,j:\mBbbZ{}].  \mforall{}[x:i  \mleq{}  j].    (x  =  <\mlambda{}x.x,  Ax,  Ax>)


By

---

Latex:
Auto

---

Home Index