fact: Definition coherent I A (M:family I A) (K:I->Prop) (u:I->A) := forall i j, K i -> K j -> family_r M j i -> family_sim M j (u j) (u i).
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)