∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α₀ α₁ α₂ : Type u₀} {β : Type u₁}
  (f : α₀ → α₁) (f' : α₁ → α₂), Bifunctor.fst f' ∘ Bifunctor.fst f = Bifunctor.fst (f' ∘ f)