proposition: Lemma dec_eq_uip {U x} (dec : forall y : U, {x = y} + {x <> y}) y (p q : x = y :> U) : p = q.
proof: Proof. etransitivity; [ | symmetry ]. { apply (dec_eq_uip' _ dec). } { etransitivity; [ apply (dec_eq_uip' _ dec) | ]. edestruct @dec_eq_adjust' as [|n]; try reflexivity. destruct (n p). } Qed.
imports: Coq.Logic.EqdepFacts Fiat.Common.Coq__8_4__8_5__Compat