+let check_if_goal_is_subsumed env (proof,menv,ty) table =
+ match ty with
+ | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
+ when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
+ (let goal_equation = 0,proof,(eq_ty,left,right,Eq),menv in
+ match Indexing.subsumption env table goal_equation with
+ | Some (subst, (_,p,_,m)) ->
+ let p = Inference.apply_subst subst (Inference.build_proof_term p) in
+ let newp =
+ let rec repl = function
+ | Inference.ProofGoalBlock (_, gp) ->
+ Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
+ | Inference.NoProof -> Inference.BasicProof ([],p)
+ | Inference.BasicProof _ -> Inference.BasicProof ([],p)
+ | Inference.SubProof (t, i, p2) ->
+ Inference.SubProof (t, i, repl p2)
+ | _ -> assert false
+ in
+ repl proof
+ in
+ Some (newp,Inference.apply_subst_metasenv subst m @ menv)
+ | None -> None)
+ | _ -> None
+;;
+