proposition: Theorem Fix_equiv : forall x : A, r (Fix Rwf P F x) (@F x (fun (y : A) (_ : R y x) => Fix Rwf P F y)).
proof: Proof. intro x; unfold Fix. rewrite <- Fix_F_eq. apply Hstep; intros. apply Fix_F_equiv_inv. Qed.
imports: Coq.Classes.RelationClasses