Lemma transportf_sec_constant {A B : UU} {C : A -> B -> UU} {x1 x2 : A} (p : x1 = x2) (f : ∏ y : B, C x1 y) : (transportf (λ x, ∏ y : B, C x y) p f) = (λ y, transportf (λ x, C x y) p (f y)). Proof. induction p; reflexivity. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.