fact: Definition local_limit_dep I A {IA:Inhab A} (M:family I A) (i:I) (u:forall j, family_r M j i -> A) := epsilon (fun l => forall j, match classicT (family_r M j i) with | left m => family_sim M j (u j m) l | right _ => True end).
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)