proposition: Lemma FixVal_fix_inv : forall I A {IA:Inhab A} (M:family I A) (E:binary A) (F:A->A) (Q:I->A->Prop) (x:A), x = FixVal F -> eq = similar M -> COFE M -> continuous M Q -> contractive M F Q -> x = F x /\ forall i, (Q i x).
proof: Proof. Proof using. intros. applys* FixValMod_fix_inv. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)