(ProofEngineHelpers.compare_metasenvs
~newmetasenv:metasenv ~oldmetasenv:proof_menv) in
let goal_proof, side_effects_t =
- let initial = (* Equality.add_subst subsumption_subst*) newproof in
+ let initial = Equality.add_subst subsumption_subst newproof in
Equality.build_goal_proof bag
eq_uri goalproof initial type_of_goal side_effects
context proof_menv