proposition: Lemma FixFunMod_corec_inv : forall I A B (M:family I B) (P:A->Prop) (S:I->B->Prop) {IB:Inhab B} (E:binary B) (F:(A->B)->(A->B)) (f:A->B), f = FixFunMod E F -> E = similar M -> COFE M -> (forall i y1 y2, S i y1 -> (forall j, family_r M j i -> family_sim M j y1 y2) -> S i y2) -> corec_contractive M P F S -> (forall x, P x -> E (f x) (F f x)) /\ (forall x i, P x -> S i (f x)).
proof: Proof. Proof using. introv Deff SimE Cofe Conti Contr. eapply FixFunMod_mixed_partial_inv with (S:=fun i x y => S i y) (R:=@empty A); autos~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)