proposition: Lemma by_cases_property : forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T), by_cases_pr a b (by_cases a b).
proof: Proof. ir. cp (by_cases_exists a b). cp (by_cases_nonempty a b). cp (chooseT_pr H0 H). unfold by_cases in |- *. assert (by_cases_nonempty a b = H0). ap proof_irrelevance. rewrite H2. am. Qed.
imports: tactics