make semantics of equality of literals require matching types

(type inferencer and soundness not updated)
open semanticPrimitivesTheory in intLangProofScript.sml
fix a proof for changed equality semantics
fix another proof for change to equality semantics
update proof of do_Ceq_to_bc_equal