fact: Fixpoint FixR_F (x:A)(Hx : E x)(a: Acc (restrict E R)x ) : P x := F _ Hx (fun (y:A) (h0 : E y) (h : R y x) => FixR_F y (restriction_fwd y x (restrict_build y x h0 Hx h)) (Acc_inv a (restrict_build y x h0 Hx h))).
imports: Coq(Wellfounded Ensembles Relations)