fact: Definition partialize A B (F:(A->B)->(A->B)) : (A-->B)->(A-->B) := fun fp => let (f,P) := fp in Build_partial (F f) P.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)