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