Definition maponpaths_pr1_pr2 {X} {P:X->UU} {Q:∏ x, P x->Type} {w w': ∑ x p, Q x p} (p : w = w') : transportf P (maponpaths pr1 p) (pr1 (pr2 w)) = pr1 (pr2 w'). Proof. intros. induction p. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.