fact: Definition contractive I A (M:family I A) (F:A->A) (Q:I->A->Prop) := forall i x y, (forall j, family_r M j i -> family_sim M j x y /\ Q j x /\ Q j y) -> family_sim M i (F x) (F y) /\ Q i (F x).
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)