theory LF
imports "../Nominal2"
begin

atom_decl name
atom_decl ident

nominal_datatype lf:
    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 lf.distinct
thm lf.induct
thm lf.inducts
thm lf.exhaust
thm lf.strong_exhaust
thm lf.fv_defs
thm lf.bn_defs
thm lf.perm_simps
thm lf.eq_iff
thm lf.fv_bn_eqvt
thm lf.size_eqvt
thm lf.supports
thm lf.fsupp
thm lf.supp
thm lf.fresh
thm lf.fresh[simplified]



end