---

Step * of Lemma eq_knd_self

∀[k:Knd]. (k = k ~ tt)
BY
{ (Auto THEN BLemma `eqtt_to_assert` THEN Auto) }

1
1. k : Knd
⊢ ↑k = k

---

Latex:


\mforall{}[k:Knd].  (k  =  k  \msim{}  tt)


By

(Auto  THEN  BLemma  `eqtt\_to\_assert`  THEN  Auto)

---

Home Index