proposition: Lemma vcomp_move_R_Mp {C : bicat} {X Y : C} {f g h : C⟦X,Y⟧} (η₁ : f ==> g) (η₂ : f ==> h) (ε : g ==> h) (Hε : is_invertible_2cell ε) : η₁ = Hε^-1 o η₂ -> ε o η₁ = η₂.
proof: Proof. intro. rewrite <- (id2_right η₂). rewrite <- (vcomp_linv Hε). rewrite vassocr. apply maponpaths_2. assumption. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat