proposition: Lemma FixR_F_eq : forall (x:A)(Hx : E x) (r: Acc (restrict E R) 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 r (restrict_build y x h0 Hx h)))= FixR_F x Hx r.
proof: Proof. destruct r using Acc_inv_dep; auto. Qed.
imports: Coq(Wellfounded Ensembles Relations)