proposition: Lemma inj_ex_intro : forall P (x : A) p q, ex_intro P x p = ex_intro P x q -> p = q.
proof: Proof. intros. apply inj_right_pair with (A:=A). intros x0 y0; case (eq_dec x0 y0); [left|right]; hyp. hyp. Qed.
imports: Coq(Structures.Equalities) CoLoR(LogicUtil RelUtil BoolUtil)