theory LFex
imports "Parser"
begin

atom_decl name
atom_decl ident

ML {* val _ = cheat_fv_rsp := false *}
ML {* val _ = cheat_alpha_bn_rsp := false *}
ML {* val _ = cheat_equivp := false *}

nominal_datatype kind =
    Type
  | KPi "ty" n::"name" k::"kind" bind n in k
and ty =
    TConst "ident"
  | TApp "ty" "trm"
  | TPi "ty" n::"name" t::"ty" bind n in t
and trm =
    Const "ident"
  | Var "name"
  | App "trm" "trm"
  | Lam "ty" n::"name" t::"trm" bind n in t

thm kind_ty_trm.supp

end