proposition: Lemma constructive_indefinite_ground_description : (exists x : A, P x) -> {x : A | P x}.
proof: Proof. intro H. assert (H1 : exists n : nat, P' n). { destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption. } apply (constructive_indefinite_ground_description_nat P' P'_decidable) in H1. destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption. Defined.
imports: Arith