---

Step * of Lemma comparison-linear

∀[T:Type]. ∀cmp:comparison(T). Linorder(cmp-type(T;cmp);x,y.cmp-le(cmp;x;y))
BY
{ TACTIC:(Auto THEN RepeatFor 2 (D 0)) }

1
1. [T] : Type
2. cmp : comparison(T)
⊢ Refl(cmp-type(T;cmp);x,y.cmp-le(cmp;x;y))

2
1. [T] : Type
2. cmp : comparison(T)
⊢ Trans(cmp-type(T;cmp);x,y.cmp-le(cmp;x;y)) ∧ AntiSym(cmp-type(T;cmp);x,y.cmp-le(cmp;x;y))

3
1. [T] : Type
2. cmp : comparison(T)
3. x : cmp-type(T;cmp)
⊢ ∀y:cmp-type(T;cmp). (cmp-le(cmp;x;y) ∨ cmp-le(cmp;y;x))

4
.....wf..... 
1. T : Type
2. cmp : comparison(T)
⊢ istype(cmp-type(T;cmp))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}cmp:comparison(T).  Linorder(cmp-type(T;cmp);x,y.cmp-le(cmp;x;y))


By

---

Latex:
TACTIC:(Auto  THEN  RepeatFor  2  (D  0))

---

Home Index