proposition: Theorem dep_non_dep_functional_rel_reification : DependentFunctionalRelReification -> FunctionalRelReification.
proof: Proof. intros DepFunReify A B R H. destruct (DepFunReify A (fun _ => B) R H) as (f,Hf). exists f; trivial. Qed.
imports: RelationClasses Logic Wf_nat Decidable