fact: Definition partial_fixed_point' A B (E:binary B) (F:(A->B)->(A->B)) (f:A-->B) := fixed_point (partial_equiv E) (partialize F) f.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)