Correctness_Algebras.Relative_Domain