Function summarize_proof_with 

pub fn summarize_proof_with(
    trace: &ProofTrace,
    register: Register,
    overlay: Option<&'static DomainGloss>,
) -> Option<String>

As summarize_proof, but renders under a domain-gloss overlay (curated examples read in real domain terms; None = the dictionary-fallback default).