proposition: Lemma by_cases_nonempty : forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T), nonemptyT T.
proof: Proof. ir. ir. assert (P \/ ~ P). ap p_or_not_p. nin H. eapply nonemptyT_intro. exact (a H). eapply nonemptyT_intro. exact (b H). Qed.
imports: tactics