equal
deleted
inserted
replaced
33 as ~~bn as' /\ EX pi. (bn as, t) ~~lst (bn as', t') |
33 as ~~bn as' /\ EX pi. (bn as, t) ~~lst (bn as', t') |
34 |
34 |
35 (both are equivalent, but the second seems to be closer to |
35 (both are equivalent, but the second seems to be closer to |
36 the fv-function) |
36 the fv-function) |
37 |
37 |
|
38 - when there are more than one shallow binder, then alpha |
|
39 equivalence creates more than one permutation. According |
|
40 to the paper, this is incorrect. |
|
41 |
|
42 Example in TestMorePerm. |
|
43 |
|
44 |
38 - nested recursion, like types "trm list" in a constructor |
45 - nested recursion, like types "trm list" in a constructor |
39 |
46 |
40 - define permute_bn automatically and prove properties of it |
47 - define permute_bn automatically and prove properties of it |
41 |
48 |
42 - prove renaming-of-binders lemmas |
49 - prove renaming-of-binders lemmas |