fact: Definition mixed_contractive I A B (M:family I B) (P:A->Prop) (F:(A->B)->(A->B)) (R:binary A) (S:I->A->B->Prop) := forall i x f1 f2, P x -> (forall y j, P y -> lexico2 (family_r M) R (j,y) (i,x) -> family_sim M j (f1 y) (f2 y) /\ S j y (f1 y) /\ S j y (f2 y)) -> family_sim M i (F f1 x) (F f2 x) /\ S i x (F f1 x).
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)