---

Step * of Lemma le_witness_for_triv

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

---

Latex:

---

Latex:
\mforall{}[i,j:\mBbbZ{}].    <\mlambda{}x.Ax,  Ax,  Ax>  \mmember{}  i  \mleq{}  j  supposing  i  \mleq{}  j


By

---

Latex:
Auto

---

Home Index