proposition: Lemma constructive_definite_descr_fun_reification : ConstructiveDefiniteDescription -> FunctionalRelReification.
proof: Proof. intros DefDescr A B R H. exists (fun x => proj1_sig (DefDescr B (R x) (H x))). intro x. apply (proj2_sig (DefDescr B (R x) (H x))). Qed.
imports: RelationClasses Logic Wf_nat Decidable