proposition: Lemma relative_non_contradiction_of_indefinite_descr : forall C:Prop, (ConstructiveIndefiniteDescription -> C) -> (FunctionalChoice -> C).
proof: Proof. intros C H AC_fun. assert (AC_depfun := non_dep_dep_functional_choice AC_fun). pose (A0 := { A:Type & { P:A->Prop & exists x, P x }}). pose (B0 := fun x:A0 => projT1 x). pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y). pose (H0 := fun x:A0 => projT2 (projT2 x)). destruct (AC_depfun A0 B0 R0 H0) as (f, Hf). apply H. intros A P H'. exists (f (existT _ A (existT _ P H'))). pose (Hf' := Hf (existT _ A (existT _ P H'))). assumption. Qed.
imports: RelationClasses Logic Wf_nat Decidable