fact: Definition locally_complete I A (M:family I A) := forall u i, locally_coherent M i u -> exists l, local_limit M i u l.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)