Function prove_equivalence 

pub fn prove_equivalence(a: &ProofExpr, b: &ProofExpr) -> EquivOutcome

Are a and b equivalent? F ≡ S iff F ↔ S is valid, i.e. ¬(F ↔ S) is UNSAT.

One solve discharges both outcomes: a satisfying assignment is the counterexample (Differ); UNSAT is RUP-certified into Equivalent (the certified trust tier — a solver bug that can’t be replayed yields Unsupported, never a false Equivalent). Structurally identical formulas short-circuit with no solve at all.