theory Foo2imports "../Nominal2" begin(* Contrived example that has more than one binding clause*)atom_decl namenominal_datatype foo: trm = Var "name"| App "trm" "trm"| Lam x::"name" t::"trm" bind x in t| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2| Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2and assg = As_Nil| As "name" x::"name" t::"trm" "assg" binder bn::"assg \<Rightarrow> atom list"where "bn (As x y t a) = [atom x] @ bn a"| "bn (As_Nil) = []"thm foo.bn_defsthm foo.permute_bnthm foo.perm_bn_alphathm foo.perm_bn_simpsthm foo.bn_finitethm foo.distinctthm foo.inductthm foo.inductsthm foo.strong_inductthm foo.exhaustthm foo.strong_exhaustthm foo.fv_defsthm foo.bn_defsthm foo.perm_simpsthm foo.eq_iffthm foo.fv_bn_eqvtthm foo.size_eqvtthm foo.supportsthm foo.fsuppthm foo.suppthm foo.freshthm foo.sizeend