∀ {n : ℕ} {α β γ : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [inst : MvFunctor F] [LawfulMvFunctor F] (g : α.Arrow β)
  (h : β.Arrow γ) (x : F α), MvFunctor.map h (MvFunctor.map g x) = MvFunctor.map (TypeVec.comp h g) x