{μ : YoungDiagram} →
  {motive : SemistandardYoungTableau μ → Sort u} →
    (t : SemistandardYoungTableau μ) →
      ((entry : ℕ → ℕ → ℕ) →
          (row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2) →
            (col_strict' : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry i1 j < entry i2 j) →
              (zeros' : ∀ {i j : ℕ}, (i, j) ∉ μ → entry i j = 0) →
                motive { entry := entry, row_weak' := row_weak', col_strict' := col_strict', zeros' := zeros' }) →
        motive t