proposition: Lemma simplification_sigma2_uip@{i j |} {A : Type@{i}} {uip : UIP A} {P : A -> Type@{i}} {B : Type@{j}} (p : A) (x y : P p) : (x = y -> B) -> ((p , x) = (p, y) -> B).
proof: Proof. intros t e. apply t. exact (pr2_uip@{i} e). Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec