Function bounded_to_proof 

pub fn bounded_to_proof(e: &BoundedExpr) -> Option<ProofExpr>

Lower a Boolean-fragment BoundedExpr to ProofExpr, or None for any node outside the propositional fragment (integers, bitvectors, arrays, ordered comparisons, quantifiers, uninterpreted applications) — those require bit-blasting, not direct lowering.