proposition: Lemma Eq_rect_eq_UIP_ U : Eq_rect_eq U -> UIP_ U.
proof: Proof. lazy; intro H. intros x y p1 p2. destruct p2. specialize (H x (fun y => x = y) eq_refl p1); simpl in *. rewrite <- Eq_rect_eq_UIP_helper in H. symmetry; assumption. Qed.
imports: Coq.Logic.EqdepFacts Fiat.Common.Coq__8_4__8_5__Compat