proposition: Lemma pr2_transportf {A} {B1 B2 : A → UU} {a a' : A} (e : a = a') (xs : B1 a × B2 a) : pr2 (transportf (λ a, B1 a × B2 a) e xs) = transportf _ e (pr2 xs).
proof: Proof. apply pathsinv0. apply (transport_map (λ a, pr2 (P := λ _, B2 a))). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics