proposition: Theorem non_dep_dep_functional_rel_reification : FunctionalRelReification -> DependentFunctionalRelReification.
proof: Proof. intros AC_fun A B R H. pose (B' := { x:A & B x }). pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)). destruct (AC_fun A B' R') as (f,Hf). - intros x. destruct (H x) as (y,(Hy,Huni)). exists (existT (fun x => B x) x y). repeat split; trivial. intros (x',y') (Heqx',Hy'). simpl in *. destruct Heqx'. rewrite (Huni y'); trivial. - exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))). intro x; destruct (Hf x) as (Heq,HR) using and_indd. destruct (f x); simpl in *. destruct Heq using eq_indd; trivial. Qed.
imports: RelationClasses Logic Wf_nat Decidable