proposition: Lemma Eq_rect_eq_UIP_helper {U x y} (p : x = y :> U) : p = match p in (_ = y) return (x = y) with eq_refl => eq_refl end.
proof: Proof. destruct p; reflexivity. Defined.
imports: Coq.Logic.EqdepFacts Fiat.Common.Coq__8_4__8_5__Compat