proposition: Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s.
proof: Proof. intro x; induction (Rwf x); intros. rewrite <- 2 Fix_F_eq; intros. apply F_ext; intros []; auto. Qed.
imports: Coq.Init.Wf Coq.Program.Utils