1 theory Minimal

     2 imports "../Nominal/Nominal2"

     3 begin

     4 

     5 atom_decl name

     6 

     7 nominal_datatype lam =

     8   Var "name"

     9 | App "lam" "lam"

    10 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)

    11 

    12 lemma alpha_test:

    13   shows "Lam [x]. (Var x) = Lam [y]. (Var y)"

    14   by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)

    15 

    16 end