HOL.Alethe_Builtin_Rewrites