proposition: Lemma FixVal_fix : forall I A {IA:Inhab A} (M:family I A) (E:binary A) (F:A->A) (x:A), x = FixVal F -> eq = similar M -> COFE M -> contractive_noinv M F -> x = F x.
proof: Proof. Proof using. intros. applys* (@FixValMod_fix _ _ M _ eq). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)