theory LF
imports "../NewParser"
begin

declare [[STEPS = 9]]

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" 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