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 : Id@{i} p q, Id (@Id_rew@{i i} A p P x q e) y -> B) -> (Id ((p, x)) ((q, y)) -> B).
proof: Proof. intros. revert X. change p with (pr1 (p, x)). change q with (pr1 (q, y)). change x with (pr2 (p, x)) at 3. change y with (pr2 (q, y)) at 4. destruct X0. intros X. eapply (X id_refl). apply id_refl. Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec