equal
deleted
inserted
replaced
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 nominal_datatype lam = |
7 nominal_datatype lam = |
8 Var "name" |
8 Var "name" |
9 | App "lam" "lam" |
9 | App "lam" "lam" |
10 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
10 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
11 |
11 |
12 lemma fresh_fun_eqvt_app3: |
12 lemma fresh_fun_eqvt_app3: |
13 assumes a: "eqvt f" |
13 assumes a: "eqvt f" |
14 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
14 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
15 shows "a \<sharp> f x y z" |
15 shows "a \<sharp> f x y z" |