proposition: Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x.
proof: Proof. intros x [n fxn]; generalize dependent x. pattern n; apply lt_wf_ind; intros n0 H x fxn. constructor; intros y H0. destruct (F_compat y x) as (x0,H1,H2); trivial. apply (H x0); auto. Qed.
imports: PeanoNat