check whether the "weirdo" example from the binding bestiary works with shallow binders
theory TestMorePerm
imports "../Parser"
begin
text {*
"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 name
nominal_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 p3
thm 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