proposition: Lemma simplification_sigma1_nondep_dep@{i j |} {A : Type@{i}} {P : Type@{i}} (p q : A) (x : P) (y : P) {B : (p, x) = (q, y) -> Type@{j}} : (forall e' : p = q, forall e : x = y, B (pack_sigma_nondep 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 2 4. change y with (q, y).2 at 2 4. 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