fact: Definition consistent A B (E:binary B) (f f': A-->B) := pfun_equiv E (pred_and (dom f) (dom f')) f f'.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)