fact: 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').
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics