Correctness_Algebras.Extended_Designs