{P : Sort u} →
  {k : ℤ} →
    {h : Lean.Expr} →
      {k' : ℤ} →
        {h' : Lean.Expr} →
          Lean.Meta.Grind.Arith.Cutsat.MulEqProof.const✝ k h = Lean.Meta.Grind.Arith.Cutsat.MulEqProof.const✝¹ k' h' →
            (k = k' → h = h' → P) → P