There has been a lot of work on "hammers" for various systems. E.g. HOL(y)hammer. https://link.springer.com/content/pdf/10.1007/s11786-014-0182-0.pdf They return the information they get from the SMT solver so that they can be stored in the proof scripts. This saves a lot of recomputation time. Is this feasible for EC too?