Changes

Summary

1. proper support for complex types, not just type variables (amending 623789141e39);
2. proper instantiation for make_const_proof, notably change of types for term variables;
3. tuned names;
4. more operations;