1 theory Minimal

     2 imports "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"  binds x in l ("Lam [_]. _" [100, 100] 100)

    11 

    12 

    13 

    14 lemma alpha_test:

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

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

    17 

    18 end