proposition: Lemma simplification_sigma1_dep_dep@{i j | } {A : Type@{i}} {P : A -> Type@{i}} (p q : A) (x : P p) (y : P q) {B : (p, x) = (q, y) -> Type@{j}} : (forall e' : p = q, forall e : (e' # x) = y, B (pack_sigma e' e)) -> (forall e : (p, x) = (q, y), B e).
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 5. change y with (q, y).2 at 4 6. destruct e. intros X. simpl in *. apply (X 1 1). Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec