HOL.Conditionally_Complete_Lattices