Function prove_theorem_trace 

pub fn prove_theorem_trace(input: &str) -> Result<TheoremTrace, ParseError>

Prove an English ## Theorem block and return its FOL plus a rendered PROOF TRACE. Unlike verify_theorem (which returns the raw kernel term), this surfaces the derivation tree so the proof steps are visible.