Correctness_Algebras.Pre_Post_Modal