proposition: Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
proof: Proof. intro x; induction (Rwf x); intros r s. rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros. apply F_ext; auto. Qed.
imports: Notations Ltac Logic Datatypes