Is it possible to see how
metis manages to finish a proof?
My current proof ends with:
apply (auto simp add: fun_eq_iff morph_comp_def split: if_splits) apply metis by metis
And I would like to drop the two
metis_verbose, but I don't know how to read the output,
using [[metis_trace]] by metis.
Last updated: Jul 15 2022 at 23:21 UTC