∀ {s t : Lean.Omega.Constraint} {x y : Lean.Omega.Coeffs} (a : ℤ) (j : Lean.Elab.Tactic.Omega.Justification s x) (b : ℤ)
  (k : Lean.Elab.Tactic.Omega.Justification t y) (j_1 : Lean.Elab.Tactic.Omega.Justification s x)
  (k_1 : Lean.Elab.Tactic.Omega.Justification t y),
  (Lean.Elab.Tactic.Omega.Justification.combo a j b k = Lean.Elab.Tactic.Omega.Justification.combo a j_1 b k_1) =
    (j = j_1 ∧ k = k_1)