Revert "delete some unnecessary proofs"

This reverts commit c30e3e888d5c77e52cf5f370ed252ce1291801a7.

Though these proofs have conclusions that follow from proves_soundness,
they don't require its is_set_theory assumption.
prove that context extensions preserve theory_ok
prove init_ctxt is theory_ok and has a model
work towards showing NewConst preserves consistency