Bugfix: proofs for props of non-normal arith lits (#5702)

Bugfix: proofs for props of non-normal arith lits  (#5702)

Arith has a normal form for literals, which the rewriter computes.

Nonetheless, arith sometimes gets (and ultimately propagates) non-normal
literals. It normalizes them internally and goes about its business.

However, when asked for an explanation, it must prove the non-normal
literal, rather than the normal one.

Also includes a regression for the bug, courtesy of Andy.

Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu