pub fn proof_effort(term: &Expr) -> u64
Estimate the “proof effort” metric: a rough measure of how hard it was to construct the term, based on its size and classical axiom usage.