theory LF
imports "../Nominal2"
begin

declare [[STEPS = 100]]

atom_decl name
atom_decl ident

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" ty::"ty"   bind n in ty
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