Redid simple_rewrite_conv to make it a proper conversion (returning a theorem of the for |- l=r.
Redid simple_rewrite_conv to make it a proper conversion (returning a
theorem of the for |- l=r.

Preparing theorems for use as simp-rules now works.

mwb-cde/hseq-prover