---

Step * 4 of Lemma comparison-linear

.....wf..... 
1. T : Type
2. cmp : comparison(T)
⊢ istype(cmp-type(T;cmp))
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  cmp  :  comparison(T)
\mvdash{}  istype(cmp-type(T;cmp))


By

---

Latex:
Auto

---

Home Index