proposition: Lemma FixValMod_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 = FixValMod E F -> E = similar M -> COFE M -> continuous M Q -> contractive M F Q -> E x (F x) /\ forall i, (Q i x).
proof: Proof. Proof using. introv Defx SimE Cofe Conti Contr. unfolds FixValMod, Fix. epsilon y. forwards* (y&Fixy&Inv): cofe_fixed_point. exists y. rewrite Fix_prop_eq_unique_fixed_point. rewrite~ SimE. intros [Fixy Uniy]. subst x. logic (forall U V:Prop,U->(U->V)->U/\V). apply Fixy. rewrite SimE. apply~ refl_inv. intros Ey. applys~ (>> invariant_on_fixed_point I A M F). apply~ contractive_to_invariant. rewrite~ <- SimE. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)