proposition: Theorem eq_dep_eq_dec : forall A:Type, (forall x y:A, {x = y} + {x <> y}) -> forall (P:A->Type) (p:A) (x y:P p), eq_dep A P p x p y -> x = y.
proof: Proof. Proof (fun A eq_dec => eq_rect_eq__eq_dep_eq A (eq_rect_eq_dec eq_dec)). Theorem UIP_dec : forall (A:Type), (forall x y:A, {x = y} + {x <> y}) -> forall (x y:A) (p1 p2:x = y), p1 = p2. Proof (fun A eq_dec => eq_dep_eq__UIP A (eq_dep_eq_dec eq_dec)). Unset Implicit Arguments. Module Type DecidableType. Monomorphic Parameter U:Type. Axiom eq_dec : forall x y:U, {x = y} + {x <> y}. End DecidableType. Module DecidableEqDep (M:DecidableType). Import M. 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 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_pairT2 : 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_pairT2 U eq_dep_eq. 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. intros. apply inj_right_pair. - intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption. - assumption. Qed.