proposition: Theorem constructive_indefinite_ground_description_nat_Acc : (exists n : nat, P n) -> {n : nat | P n}.
proof: Proof. intros H; apply acc_implies_P_eventually. apply P_eventually_implies_acc_ex; assumption. Defined.
imports: Arith