Lemma transportf_pair {A B} (P : A × B -> UU) {a a' : A} {b b' : B} (eA : a = a') (eB : b = b') (p : P (a,,b)) : transportf P (pathsdirprod eA eB) p = transportf (λ bb, P(a',,bb) ) eB (transportf (λ aa, P(aa,,b)) eA p). Proof. induction eA. induction eB. apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.