proposition: Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.
proof: Proof. Proof (fun eq_rect_eq P p x y => @eq_rect_eq_on__eq_dep_eq_on p P x (eq_rect_eq p P x) y). Lemma eq_dep_eq_on__UIP_on (x y : U) (p1 : x = y) : Eq_dep_eq_on (fun y => x = y) x eq_refl -> UIP_on_ x y p1. Proof. intro eq_dep_eq; red. elim p1 using eq_indd. intros p2; apply eq_dep_eq. elim p2 using eq_indd. apply eq_dep_intro. Qed.