∀ {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [inst : MvFunctor F] (P : α.Arrow (TypeVec.repeat n Prop))
  [LawfulMvFunctor F] (x : F α), MvFunctor.LiftP' P x ↔ ∃ u, MvFunctor.map (TypeVec.subtypeVal P) u = x