Lemma transportf_fun_idpath {X Y} {f:X->Y} x x' (w:x = x') (t:f x = f x) : transportf (λ x', f x' = f x) w (idpath (f x)) = maponpaths f (!w). Proof. induction w. reflexivity. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.