---

Step * 2 of Lemma int_loset_wf


UniformLinorder(ℤ;a,b.↑(a (λx,y. x ≤z y) b))
BY
{ AbReduce 0 THEN ((RW bool_to_propC 0) THENA Auto) }

1
UniformLinorder(ℤ;a,b.a ≤ b)

---

Latex:

---

Latex:

UniformLinorder(\mBbbZ{};a,b.\muparrow{}(a  (\mlambda{}x,y.  x  \mleq{}z  y)  b))


By

---

Latex:
AbReduce  0  THEN  ((RW  bool\_to\_propC  0)  THENA  Auto)

---

Home Index