Upstream or delete most of the extra_*Script.sml files in examples/miller/formalize

[ordinarymath]

There are a bunch of files in examples/miller/formalize prefixed with extra i.e.

extra_boolScript.sml
extra_listScript.sml
extra_numScript.sml
extra_pred_setScript.sml
extra_realScript.sml

This issue is taking the theorems there, upstreaming whatever is useful and then deleting or moving to their use site the remaining theorems.