Lemma transportf_comp_lemma (X : UU) (B : X -> UU) {A A' A'': X} (e : A = A'') (e' : A' = A'') (x : B A) (x' : B A') : transportf _ (e @ !e') x = x' -> transportf _ e x = transportf _ e' x'. Proof. intro H. eapply pathscomp0. 2: { apply maponpaths. exact H. } eapply pathscomp0. 2: { symmetry. apply transport_f_f. } apply (maponpaths (λ p, transportf _ p x)). apply pathsinv0. eapply pathscomp0. - apply @pathsinv0, path_assoc. - eapply pathscomp0. apply maponpaths. apply pathsinv0l. apply pathscomp0rid. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.