proposition: Theorem inj_right_pair_on (P:A -> Prop) (y y':P x) : ex_intro P x y = ex_intro P x y' -> y = y'.
proof: Proof. intros H. cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y). - simpl. destruct (eq_dec x) as [Heq|Hneq]. + elim Heq using K_dec_on; trivial. + intros. case Hneq; trivial. - case H. reflexivity. Qed.