Reflective tactics: show the reflected normal forms in the failure message via evalExpr String

For a proof-by-reflection tactic (normalize two reified sides, compare with decide +kernel), first decide in compiled code (evalExpr Bool on decide (nf a = nf b)). On failure, build showNf names 0 (nf a) as an Expr with mkAppM (names as mkListLit (mkConst String) (names.map mkStrLit), where the atom names come from ppExpr) and run unsafe evalExpr String (mkConst String) e. The printer is an ordinary mutual def over the normal-form inductive. Parenthesize an argument only if it contains a space. Users then see e.g. lhs = λ y0. g y0, rhs = λ y0. x rather than just 'false'. Lock the exact text with #guard_msgs tests. Under first | a | b, the error shown is the one from b, so put the alternative with the informative message last.