proposition: Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair.
proof: Proof. Proof (fun eq_dep_eq P p x => @eq_dep_eq_on__inj_pair2_on P p x (eq_dep_eq P p x)). End Corollaries. Notation Inj_dep_pairS := Inj_dep_pair. Notation Inj_dep_pairT := Inj_dep_pair. Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2. Module Type EqdepElimination. Axiom eq_rect_eq : forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. End EqdepElimination. Module EqdepTheory (M:EqdepElimination). Section Axioms. Variable U:Type. 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 M.eq_rect_eq U. Lemma eq_rec_eq : forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h. Proof (fun p Q => M.eq_rect_eq U p Q). Lemma eq_dep_eq : forall (P:U->Type) (p:U) (x y:P p), eq_dep 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 (UIP_refl__Streicher_K U UIP_refl). End Axioms. Lemma inj_pair2 : forall (U:Type) (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y. Proof (fun U => eq_dep_eq__inj_pair2 U (eq_dep_eq U)). Notation inj_pairT2 := inj_pair2. End EqdepTheory. Lemma f_eq_dep : forall U (P:U->Type) R p q x y (f:forall p, P p -> R p), eq_dep p x q y -> eq_dep p (f p x) q (f q y). Proof. intros * []. reflexivity. Qed.