pub fn simplify_proof_term(pt: &ProofTerm) -> ProofTerm
Perform beta/eta reduction on a proof term, returning a simplified equivalent.