theory LF
imports "../NewParser"
begin

atom_decl name
atom_decl ident

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

thm kind_ty_trm.supp

declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt]
declare alpha_gen_eqvt[eqvt]

equivariance alpha_trm_raw




end