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