HOL.Alethe_Rare_Interface