∀ {n : ℕ} {α β : TypeVec.{u} n} (F : TypeVec.{u} n → Type v) [inst : MvFunctor F] [LawfulMvFunctor F] {P : F α → Prop}
  {q : F β → Prop} (f : α.Arrow β) (g : β.Arrow α),
  TypeVec.comp f g = TypeVec.id → (∀ (u : F α), P u ↔ q (MvFunctor.map f u)) → ((∃ u, P u) ↔ ∃ u, q u)