theory Minimal
imports "Nominal2"
begin
atom_decl name
nominal_datatype lam =
Var "name"
| App "lam" "lam"
| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
lemma alpha_test:
shows "Lam [x]. (Var x) = Lam [y]. (Var y)"
by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)
end