"Well_Fnd" theory
inv_image_ind_a
inv_image_ind_tp
inv_image_ind
wellfounded_functionality_wrt_implies
wellfounded_functionality_wrt_iff