HOL.Alethe_cvc5_Rewrites