theory LetRec2
imports "../Nominal2"
begin

atom_decl name

nominal_datatype trm =
  Vr "name"
| Ap "trm" "trm"
| Lm x::"name" t::"trm"  binds (set) x in t
| Lt a::"lts" t::"trm"   binds "bn a" in a t
and lts =
  Lnil
| Lcons "name" "trm" "lts"
binder
  bn
where
  "bn Lnil = []"
| "bn (Lcons x t l) = (atom x) # (bn l)"


thm trm_lts.fv_defs
thm trm_lts.eq_iff
thm trm_lts.bn_defs
thm trm_lts.perm_simps
thm trm_lts.induct
thm trm_lts.distinct


end