22   bn::"assg \<Rightarrow> atom list"

    22   bn::"assg \<Rightarrow> atom list"

    23 where

    23 where

    24   "bn (As x y t a) = [atom x] @ bn a"

    24   "bn (As x y t a) = [atom x] @ bn a"

    25 | "bn (As_Nil) = []"

    25 | "bn (As_Nil) = []"

    26 

    26 

    27 thm foo.bn_defs

    30 thm foo.bn_defs

    28 thm foo.permute_bn

    31 thm foo.permute_bn

    29 thm foo.perm_bn_alpha

    32 thm foo.perm_bn_alpha

    30 thm foo.perm_bn_simps

    33 thm foo.perm_bn_simps

    31 thm foo.bn_finite

    34 thm foo.bn_finite

    33 

    35 

    34 thm foo.distinct

    36 thm foo.distinct

    35 thm foo.induct

    37 thm foo.induct

    36 thm foo.inducts

    38 thm foo.inducts

    37 thm foo.exhaust

    39 thm foo.exhaust