{P : Sort u} →
  {matType : ℕ → ℕ → Type} →
    {inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType} →
      {t : Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau matType} →
        {matType' : ℕ → ℕ → Type} →
          {inst' : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType'} →
            {t' : Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau matType'} →
              matType = matType' →
                inst ≍ inst' → t ≍ t' → Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau.noConfusionType P t t'