proposition: Lemma cancel_precomposition_disp {C} {D : disp_cat C} {x y z} {f : x --> y} {g g' : y --> z} {e : g' = g} {xx : D x} {yy} {zz} (ff : xx -->[f] yy) {gg : yy -->[g] zz} {gg' : yy -->[g'] zz} (ee : gg = transportf _ e gg') : ff ;; gg = transportf _ (cancel_precomposition _ _ _ _ _ _ f e) (ff ;; gg').
proof: Proof. etrans. apply maponpaths, ee. apply mor_disp_transportf_prewhisker. Qed.
imports: UniMath.Foundations.Sets UniMath.Foundations.PartD UniMath.MoreFoundations.PartA UniMath.MoreFoundations.AxiomOfChoice UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering