fact: Definition complete' I A (M:family I A) := locally_complete M /\ globally_complete M.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)