proposition: Lemma Fix_F_eq : forall (x:A) (r:Acc R x), F_sub x (fun y:{y:A | R y x} => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.
proof: Proof. intros x r; destruct r using Acc_inv_dep; auto. Qed.
imports: Coq.Init.Wf Coq.Program.Utils