+ status goalproof newproof subsumption_id subsumption_subst proof_menv
+ in
+ let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
+ let newmetasenv =
+ other_menv @
+ List.filter
+ (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
+ in
+ let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
+ (subst, proof,gl)) subsumed_or_id
+ in