proposition: 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: Proof. induction eA. induction eB. apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics