---

Step * 1 of Lemma eq_knd_self


1. k : Knd
⊢ ↑k = k
BY
{ (Unfold `eq_knd` 0 THEN RWO "deq_property<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  Knd
\mvdash{}  \muparrow{}k  =  k


By

---

Latex:
(Unfold  `eq\_knd`  0  THEN  RWO  "deq\_property<"  0  THEN  Auto)

---

Home Index