theory TestMorePermimports "../Parser"begintext {* "Weirdo" example from Peter Sewell's bestiary. In case of deep binders, it is not coverd by our approach of defining alpha-equivalence with a single permutation. Check whether it works with shallow binders as defined below.*}ML {* val _ = cheat_equivp := true *}atom_decl namenominal_datatype foo = Foo_var "name"| Foo_pair "foo" "foo" | Foo x::"name" y::"name" p1::"foo" p2::"foo" p3::"foo" bind x in p1, bind x in p2, bind y in p2, bind y in p3thm alpha_foo_raw.intros[no_vars]thm permute_weird_raw.simps[no_vars]thm alpha_weird_raw.intros[no_vars]thm fv_weird_raw.simps[no_vars]end