HOL.Complete_Partial_Order