---

Step * 1 of Lemma comparison-linear


1. [T] : Type
2. cmp : comparison(T)
⊢ Refl(cmp-type(T;cmp);x,y.cmp-le(cmp;x;y))
BY
{ (D 0 THEN Auto THEN Unfold `cmp-le` 0) }

1
1. [T] : Type
2. cmp : comparison(T)
3. a : cmp-type(T;cmp)
⊢ 0 ≤ (cmp a a)

---

Latex:

---

Latex:

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


By

---

Latex:
(D  0  THEN  Auto  THEN  Unfold  `cmp-le`  0)

---

Home Index