proposition: Lemma eq_rect_eq : forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
proof: Proof. Proof eq_rect_eq_dec eq_dec. Theorem eq_dep_eq : forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y. Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq). Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2. Proof (eq_dep_eq__UIP U eq_dep_eq). Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x. Proof (UIP__UIP_refl U UIP). Lemma Streicher_K : forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. Proof (K_dec_type eq_dec). Lemma inj_pairP2 : forall (P:U -> Prop) (x:U) (p q:P x), ex_intro P x p = ex_intro P x q -> p = q. Proof N.inj_pairP2. Lemma inj_pair2 : forall (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y. Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq. Notation inj_pairT2 := inj_pair2. End DecidableEqDepSet. Lemma inj_pair2_eq_dec : forall A:Type, (forall x y:A, {x=y}+{x<>y}) -> ( forall (P:A -> Type) (p:A) (x y:P p), existT P p x = existT P p y -> x = y ). Proof. intros A eq_dec. apply eq_dep_eq__inj_pair2. apply eq_rect_eq__eq_dep_eq. unfold Eq_rect_eq, Eq_rect_eq_on. intros; apply eq_rect_eq_dec. apply eq_dec. Qed.