- Added support for conditional equations whose premises involve
inductive sets (useful in connection with THE operator)
- Inductive and non-inductive sets (implemented as lists) can
now be mixed
- Expressed infer_derivs' in terms of infer_deriv
- Eta-expanded function instantiate to delay evaluation (avoids inefficiencies
when proof terms are switched off)