Function prove_certify_check_bounded_with_defs 

pub fn prove_certify_check_bounded_with_defs(
    premises: &[ProofExpr],
    goal: &ProofExpr,
    definitions: &[Definition],
    max_depth: usize,
) -> VerifiedProof

The depth-bounded pipeline with user definitions (Rung 0a). Definitions are validated (recursion + lowering) up front, registered as δ-unfoldable kernel definitions in the context, then the goal is proved and kernel-checked. The engine still treats the definiendum opaquely during search (Stride 3 adds expand-for-search); δ reconciles the certified term with the folded goal type at the [finish_check] root.