introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
Function definitions
- export proofs bout alpha_bn
Parser should check that:
- types of bindings match types of binding functions
- fsets are not bound in lst bindings
- bound arguments are not datatypes
- binder is referred to by name and not by type
Smaller things:
- maybe <type>_perm whould be called permute_<type>.simps;
that would conform with the terminology in Nominal2
Other:
- nested recursion, like types "trm list" in a constructor
- store information about defined nominal datatypes, so that
it can be used to define new types that depend on these