Refine_Imperative_HOL.Worklist_Subsumption_Impl