proposition: Theorem UIP_shift : forall U, UIP_refl_ U -> forall x:U, UIP_refl_ (x = x).
proof: Proof. Proof (fun U UIP_refl x => @UIP_shift_on U x (UIP_refl x)). Section Corollaries. Variable U:Type. Definition Inj_dep_pair_on (P : U -> Type) (p : U) (x : P p) := forall (y : P p), existT P p x = existT P p y -> x = y. Definition Inj_dep_pair := forall P p x, Inj_dep_pair_on P p x. Lemma eq_dep_eq_on__inj_pair2_on (P : U -> Type) (p : U) (x : P p) : Eq_dep_eq_on U P p x -> Inj_dep_pair_on P p x. Proof. intro eq_dep_eq; red; intros. apply eq_dep_eq. apply eq_sigT_eq_dep. assumption. Qed.