proposition: Lemma simplification_sigma1_nondep_dep@{i j|} {A : Type@{i}} {P : Type@{i}} (p q : A) (x : P) (y : P) {B : Id (p, x) (q, y) -> Type@{j}} : (forall e' : Id p q, forall e : Id x y, B (pack_sigma_nondep e' e)) -> (forall e : Id (sigmaI (fun _ => P) p x) (sigmaI (fun _ => P) q y), B e).
proof: Proof. intros. revert X. change p with (pr1 (p, x)). change q with (pr1 (q, y)). change x with (pr2 (p, x)) at 2 4. change y with (pr2 (q, y)) at 2 4. destruct e. intros X. simpl in *. apply (X id_refl id_refl). Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec