{P : Sort u} →
  {a? : Option Lean.Expr} →
    {cs : Array (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr)} →
      {a?' : Option Lean.Expr} →
        {cs' : Array (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr)} →
          Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul a? cs = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul a?' cs' →
            (a? = a?' → cs = cs' → P) → P