proposition: Lemma corec_rec_cofe : forall I A B {IB:Inhab B} (M:family I B) (P:A->Prop) (R:binary A), COFE M -> wf R -> COFE (corec_rec_family M P R).
proof: Proof. Proof using. introv IB Cofe WfR. apply make_COFE; simpl. typeclass. apply~ @wf_lexico2. apply~ wf_tclosure. apply~ trans_lexico2. apply trans_tclosure. intros [i x]. constructor. intros_all. destruct~ (ofe_equiv Cofe i'). intros_all. destruct~ (ofe_equiv Cofe i'). intros_all. destruct* (ofe_equiv Cofe i'). intros K u Downk Cohu. hnf in Downk. hnf in Cohu. simpls. exists (fun x => epsilon (limit M (fun i => K (i,x)) (fun i => u (i,x) x))). intros [i x] Kix. simpl. intros j x' LR' Px'. rewrite rclosure_eq_fun in *. epsilon l. apply (cofe_complete Cofe). introv H H'. hnf. applys~ Downk H. introv H H' H''. applys~ (>> Cohu H H'). intros L. hnf in L. simpl in L. destruct LR' as [LR'|Ex'x]. asserts Kjx': (K (j,x')). apply* Downk. apply~ trans_sym_rl. applys~ (>> Cohu Kix Kjx' LR'). inversion Ex'x. subst x. apply~ L. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)