proposition: Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_.
proof: Proof. Proof (fun eq_dep_eq x y p1 => @eq_dep_eq_on__UIP_on x y p1 (eq_dep_eq _ _ _)). Lemma UIP_on__UIP_refl_on (x : U) : UIP_on_ x x eq_refl -> UIP_refl_on_ x. Proof. intro UIP; red; intros; symmetry; apply UIP. Qed.