Correctness_Algebras.Domain