Function refinement_info_for 

pub fn refinement_info_for<'a>(
    type_name: &str,
    inputs: &ProofLowerInputs<'a>,
) -> Option<RefinementInfo<'a>>

Inspect inputs for a refinement-via-opaque record by type_name. Returns Some(info) iff there’s exactly one matching smart constructor and the record has a single carrier field.

Defaults to “any scope” — walks entry + every dep module’s type_defs and fn_defs to find the record + smart constructor. Use refinement_info_for_in_scope when two modules declare a refined record of the same bare name (A.Natural vs B.Natural) and you need each scope’s own predicate; the unscoped form returns whichever record walked first.