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 (pr1 (p, x)). change q with (pr1 (q, y)). change x with (pr2 (p, x)) at 2. change y with (pr2 (q, y)) at 2. destruct eq. intros eq. exact (eq 1 1). Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec