proposition: Lemma by_cases_unique : forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (x : T), by_cases_pr a b x -> by_cases a b = x.
proof: Proof. ir. cp (by_cases_property a b). ir. assert (P \/ ~ P). ap p_or_not_p. nin H1. unfold by_cases_pr in H. unfold by_cases_pr in H0. xd. transitivity (a H1). sy. au. au. unfold by_cases_pr in H. unfold by_cases_pr in H0. xd. transitivity (b H1). sy. au. au. Qed.
imports: tactics