proposition: Lemma by_cases_if_not : forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (q : ~ P), by_cases a b = b q.
proof: Proof. ir. eapply by_cases_unique. unfold by_cases_pr in |- *. xd. ir. cp (q p). elim H. ir. assert (q = q0). ap proof_irrelevance. rewrite H. tv. Qed.
imports: tactics