proposition: Lemma Fix_F_inv : forall (x : A) (r s : Acc R x), Fix_F x r = Fix_F x s.
proof: Proof. intro x; elim (Rwf x); intros. rewrite (Fix_F_eq x0 r); rewrite (Fix_F_eq x0 s); intros. apply F_ext; auto. Qed.
imports: Arith Omega List