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