{𝕜 : Type u_1} →
  {B : Type u_2} →
    {F : Type u_4} →
      {E : B → Type u_6} →
        [inst : NontriviallyNormedField 𝕜] →
          {EB : Type u_7} →
            [inst_1 : NormedAddCommGroup EB] →
              [inst_2 : NormedSpace 𝕜 EB] →
                {HB : Type u_8} →
                  [inst_3 : TopologicalSpace HB] →
                    {IB : ModelWithCorners 𝕜 EB HB} →
                      [inst_4 : TopologicalSpace B] →
                        [inst_5 : ChartedSpace HB B] →
                          [inst_6 : (x : B) → AddCommMonoid (E x)] →
                            [inst_7 : (x : B) → Module 𝕜 (E x)] →
                              [inst_8 : NormedAddCommGroup F] →
                                [inst_9 : NormedSpace 𝕜 F] →
                                  [inst_10 : (x : B) → TopologicalSpace (E x)] →
                                    {a : VectorPrebundle 𝕜 F E} →
                                      {n : WithTop ℕ∞} →
                                        {motive : VectorPrebundle.IsContMDiff IB a n → Sort u} →
                                          (t : VectorPrebundle.IsContMDiff IB a n) →
                                            ((exists_contMDiffCoordChange :
                                                  ∀ e ∈ a.pretrivializationAtlas,
                                                    ∀ e' ∈ a.pretrivializationAtlas,
                                                      ∃ f,
                                                        ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n f
                                                            (e.baseSet ∩ e'.baseSet) ∧
                                                          ∀ b ∈ e.baseSet ∩ e'.baseSet,
                                                            ∀ (v : F),
                                                              (f b) v = (↑e' { proj := b, snd := e.symm b v }).2) →
                                                motive ⋯) →
                                              motive t