Step * of Lemma kind-rename_wf

[ra,rt:Id ─→ Id]. ∀[k:Knd].  (kind-rename(ra;rt;k) ∈ Knd)
BY
(Unfold `kind-rename` 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