proposition: Corollary fun_reification_descr_computational_excluded_middle_in_prop_context : FunctionalRelReification -> (forall P:Prop, P \/ ~ P) -> forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
proof: Proof. intros FunReify EM C H. intuition auto using constructive_definite_descr_excluded_middle, (relative_non_contradiction_of_definite_descr (C:=C)). Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid