proposition: Lemma eq_rect_eq_on__eq_dep1_eq_on (p : U) (P : U -> Type) (y : P p) : Eq_rect_eq_on p P y -> forall (x : P p), eq_dep1 p x p y -> x = y.
proof: Proof. intro eq_rect_eq. simple destruct 1; intro. rewrite <- eq_rect_eq; auto. Qed.