proposition: Lemma relative_non_contradiction_of_definite_descr : forall C:Prop, (ConstructiveDefiniteDescription -> C) -> (FunctionalRelReification -> C).
proof: Proof. intros C H FunReify. assert (DepFunReify := non_dep_dep_functional_rel_reification FunReify). 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 (DepFunReify 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