proposition: Lemma Fix_eq : forall x, Fix x == F (fun y (p : R y x) => Fix y).
proof: Proof. intro x; unfold Wf.Fix. rewrite <- Fix_F_eq. apply F_ext; intros. apply Fix_F_inv. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil) Coq(List)