proposition: Lemma rec_cofe : forall A B {IB:Inhab B} (E:binary B) (P:A->Prop) (R:binary A), equiv E -> wf R -> COFE (rec_family E P R).
proof: Proof. Proof using. introv IB Equiv WfR. apply make_COFE; simpl. typeclass. apply~ wf_tclosure. apply trans_tclosure. destruct Equiv. constructor; intros_all*. intros K u Downk Cohu. hnf in Downk. hnf in Cohu. simpls. exists (fun x => u x x). intros x Kx. simpl. intros x' Px'. rewrite rclosure_eq. intros [Ex'x|x'x]. apply equiv_sym; auto. apply* Cohu. subst. apply~ equiv_refl. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)