HOL.Alethe_Boolean_Rewrites_Lemmas