{P : Sort u} →
  {k : ℤ} →
    {y? : Option Int.Linear.Var} →
      {c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr} →
        {k' : ℤ} →
          {y?' : Option Int.Linear.Var} →
            {c' : Lean.Meta.Grind.Arith.Cutsat.EqCnstr} →
              Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div k y? c =
                  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div k' y?' c' →
                (k = k' → y? = y?' → c = c' → P) → P