∀ (n : ℕ) {β : (v : TypeVec.{u_1} (n + 1)) → (v' : TypeVec.{u_2} (n + 1)) → v.Arrow v' → Sort u_3}
  (v : TypeVec.{u_1} (n + 1)) (v' : TypeVec.{u_2} (n + 1)),
  ((fs : (v.drop ::: v.last).Arrow v') → β (v.drop ::: v.last) v' fs) =
    ((fs : (v.drop ::: v.last).Arrow (v'.drop ::: v'.last)) → β (v.drop ::: v.last) (v'.drop ::: v'.last) fs)