Lemma transportf_paths_FlFr {A B : UU} {f g : A -> B} {x1 x2 : A} (p : x1 = x2) (q : f x1 = g x1) : transportf (λ x, f x = g x) p q = !maponpaths f p @ q @ maponpaths g p. Proof. induction p. cbn. apply pathsinv0. apply pathscomp0rid. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.