HOL.BNF_Fixpoint_Base