proposition: Lemma simplification_sigma1@{i j |} {A : Type@{i}} {P : Type@{i}} {B : Type@{j}} (p q : A) (x : P) (y : P) : (p = q -> x = y -> B) -> ((p, x) = (q, y) -> B).
proof: Proof. intros * prf eq; revert prf. change p with ((p, x).1). change q with ((q, y).1). change x with ((p, x).2) at 2. change y with ((q, y).2) at 2. destruct eq. intros eq. exact (eq 1 1). Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec