proposition: Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}.
proof: Proof. intros Acc_0. pattern 0. apply Fix_F with (R := R); [| assumption]. clear Acc_0; intros x IH. destruct (P_decidable x) as [Px | not_Px]. - exists x; simpl; assumption. - set (y := S x). assert (Ryx : R y x). + unfold R; split; auto. + destruct (IH y Ryx) as [n Hn]. exists n; assumption. Defined.
imports: Arith