Function refinement_lift_for_given 

pub fn refinement_lift_for_given(
    given_name: &str,
    given_type: &str,
    lhs: &Spanned<Expr>,
    rhs: &Spanned<Expr>,
    ctx: &CodegenContext,
) -> Option<String>

Walk lhs/rhs looking for RecordCreate { type_name: X, fields: [(_, Ident(given_name))] } where X is a refinement record whose carrier matches given_type. Returns the refined type name when found, so callers can lift given_name’s quantifier from the carrier type to the refined type. Without this, theorems would emit ∀ (a : Int), … RecordCreate(a) … where the smart- constructor predicate has to be discharged from a’s when clause inside the theorem type — which is exactly what the previous heuristic-laden auto-proof had to work around.