HOL.Alethe_Boolean_Rewrites