fact: Definition transport_fun_path {X Y} {f g:X->Y} {x x':X} {p:x = x'} {e:f x = g x} {e':f x' = g x'} : e @ maponpaths g p = maponpaths f p @ e' -> transportf (λ x, f x = g x) p e = e'.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics