---

Step * of Lemma kind-rename_wf

∀[ra,rt:Id ─→ Id]. ∀[k:Knd].  (kind-rename(ra;rt;k) ∈ Knd)
BY
{ (Unfold `kind-rename` 0 THEN Auto) }

---

Latex:


\mforall{}[ra,rt:Id  {}\mrightarrow{}  Id].  \mforall{}[k:Knd].    (kind-rename(ra;rt;k)  \mmember{}  Knd)


By

(Unfold  `kind-rename`  0  THEN  Auto)

---

Home Index