theory SingleLetimports "../Nominal2" beginatom_decl namenominal_datatype single_let: trm = Var "name"| App "trm" "trm"| Lam x::"name" t::"trm" binds x in t| Let a::"assg" t::"trm" binds "bn a" in t| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" binds (set) x in y t t1 t2| Bar x::"name" y::"name" t::"trm" binds y x in t x y| Baz x::"name" t1::"trm" t2::"trm" binds (set) x in t1, binds (set+) x in t2 and assg = As "name" x::"name" t::"trm" binds x in tbinder bn::"assg \<Rightarrow> atom list"where "bn (As x y t) = [atom x]"thm single_let.distinctthm single_let.inductthm single_let.inductsthm single_let.exhaustthm single_let.strong_exhaustthm single_let.fv_defsthm single_let.bn_defsthm single_let.perm_simpsthm single_let.eq_iffthm single_let.fv_bn_eqvtthm single_let.size_eqvtthm single_let.supportsthm single_let.fsuppthm single_let.suppthm single_let.freshend