{F : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_3} →
      [inst : NonUnitalCStarAlgebra A₁] →
        [inst_1 : NonUnitalCStarAlgebra A₂] →
          [inst_2 : PartialOrder A₁] →
            [inst_3 : PartialOrder A₂] →
              [inst_4 : StarOrderedRing A₁] →
                [inst_5 : StarOrderedRing A₂] →
                  [inst_6 : FunLike F A₁ A₂] →
                    {motive : CompletelyPositiveMapClass F A₁ A₂ → Sort u} →
                      (t : CompletelyPositiveMapClass F A₁ A₂) →
                        ((map_cstarMatrix_nonneg' :
                              ∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑φ) →
                            motive ⋯) →
                          motive t