proposition: Lemma Fix_F_inv : forall x (r s : Acc R x), Fix_F r == Fix_F s.
proof: Proof. intro x; induction (Rwf x); intros. rewrite <- (Fix_F_eq r), <- (Fix_F_eq s); intros. apply F_ext; auto. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil) Coq(List)