proposition: Lemma Fix_F_equiv_inv : forall (x : A) (r' s' : Acc R x), r (Fix_F _ F r') (Fix_F _ F s').
proof: Proof. intro x; induction (Rwf x); intros. rewrite <- (Fix_F_eq _ F r'); rewrite <- (Fix_F_eq _ F s'); intros. eapply Hstep. eauto. Qed.
imports: Coq.Classes.RelationClasses