proposition: Lemma by_cases_exists : forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T), exists x : T, by_cases_pr a b x.
proof: Proof. ir. assert (P \/ ~ P). ap p_or_not_p. nin H. eapply ex_intro with (a H). unfold by_cases_pr in |- *. xd. ir. assert (H = p). ap proof_irrelevance. rewrite H0. tv. ir. pose (q H). elim f. eapply ex_intro with (b H). unfold by_cases_pr in |- *. xd. ir. pose (H p). elim f. ir. assert (H = q). ap proof_irrelevance. rewrite H0. tv. Qed.
imports: tactics