proposition: 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: Proof. induction w. reflexivity. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Tactics