Comment by nwah1

Simplifying and composing these proofs with other proofs should probably be the next goal. And formalizing within other computational proof paradigms.