Inductive Kind : Type :=
| KindStar : Kind (* ★ - the kind of coercions and the kind of types inhabited by [boxed] values *)
| KindArrow : Kind -> Kind -> Kind (* ⇛ - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*)
Inductive Kind : Type :=
| KindStar : Kind (* ★ - the kind of coercions and the kind of types inhabited by [boxed] values *)
| KindArrow : Kind -> Kind -> Kind (* ⇛ - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*)