{P : Sort u} →
  {n m : ℕ} →
    {t : Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix n m} →
      {n' m' : ℕ} →
        {t' : Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix n' m'} →
          n = n' → m = m' → t ≍ t' → Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix.noConfusionType P t t'