proposition: Lemma pr2_uip@{i|} {A : Type@{i}} {E : UIP A} {P : A -> Type@{i}} {x : A} {y y' : P x} : sigmaI@{i} P x y = sigmaI@{i} P x y' -> y = y'.
proof: Proof. refine (simplification_sigma1_dep_dep@{i i} _ _ _ _ _). intros e'. destruct (uip 1 e'). intros e ; exact e. Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec