proposition: Lemma FixFunMod_corec : forall I A B (M:family I B) (P:A->Prop) {IB:Inhab B} (E:binary B) (F:(A->B)->(A->B)) (f:A->B), f = FixFunMod E F -> E = similar M -> COFE M -> corec_contractive_noinv M P F -> (forall x, P x -> E (f x) (F f x)).
proof: Proof. Proof using. introv Deff SimE Cofe Contr. forwards H _: (@FixFunMod_corec_inv I A B M P post_true _ E F); autos~. intros_all~. split~. applys* Contr f1 f2. intros. forwards*: H0. subst~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)