HOL.BNF_Least_Fixpoint