proposition: Lemma invariant_on_fixed_point : forall I A (M:family I A) (F:A->A) (Q:I->A->Prop) (x:A), OFE M -> continuous M Q -> invariant M F Q -> similar M x (F x) -> forall i, Q i x.
proof: Proof. Proof using. introv Cofe Cont Inv Fixx. intros i. induction_wf IH: (ofe_wf Cofe) i. applys~ (Cont (rclosure (inverse (family_r M)) i) (fun _:I => (F x))). intros_all. apply~ sym_inv. intros j Le. apply Inv. intros k Rkj. apply IH. destruct Le. apply~ trans_inv. subst~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)