Remove redundancies such as well-formedness checks, positivity, etc.

[fiedlr]

A large portion (majority?) of the proofs consists of proving that the
pattern is well-formed, positivity, and simplifying substitutions. This is
redundant for two reasons.
a. This is a simple decision procedure that's linear in the size of the
term, so there's no reason to include it in the certificate.
b. Once we have proved well-formedness for the initial goals, applications
of axioms maintains this invariant.