proposition: Lemma FixFunMod_corec_total : forall I A B (M:family I B) {IB:Inhab B} (E:B->B->Prop) (F:(A->B)->(A->B)) (f:A->B), f = FixFunMod E F -> E = similar M -> COFE M -> (forall i x f1 f2, (forall y j, family_r M j i -> family_sim M j (f1 y) (f2 y)) -> family_sim M i (F f1 x) (F f2 x)) -> (forall x, E (f x) (F f x)).
proof: Proof. Proof using. intros. asserts~ K: (pred_true x). gen x. apply* FixFunMod_corec. intros_all~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)