proposition: Lemma simplification_sigma1_dep@{i j |} {A : Type@{i}} {P : A -> Type@{i}} {B : Type@{j}} (p q : A) (x : P p) (y : P q) : (forall e : paths@{i} p q, paths (transport@{i i} P e x) y -> B) -> ((p, x) = (q, y) -> B).
proof: Proof. intros. revert X. change p with (p, x).1. change q with (q, y).1. change x with ((p, x).2) at 3. change y with ((q, y).2) at 4. destruct X0. intros X. eapply (X 1). apply 1. Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec