presented at event 9th International Conference on Interactive Theorem Proving (ITP) Held as Part of the Federated Logic Conference (FloC) Conference