proposition: Theorem eq_proofs_unicity A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A) : forall (y:A) (p1 p2:x = y), p1 = p2.
proof: Proof. Proof (@eq_proofs_unicity_on A x (eq_dec x)). Theorem K_dec A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A) : forall P:x = x -> Prop, P (eq_refl x) -> forall p:x = x, P p. Proof (@K_dec_on A x (eq_dec x)). Theorem inj_right_pair A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A) : forall (P:A -> Prop) (y y':P x), ex_intro P x y = ex_intro P x y' -> y = y'. Proof (@inj_right_pair_on A x (eq_dec x)). Require Import EqdepFacts. Theorem K_dec_type (A:Type) (eq_dec:forall x y:A, {x = y} + {x <> y}) (x:A) (P:x = x -> Prop) (H:P (eq_refl x)) (p:x = x) : P p. Proof. elim p using K_dec. - intros x0 y; case (eq_dec x0 y); [left|right]; assumption. - trivial. Qed.