∀ {h : Lean.Expr} {x : Int.Linear.Var} {e' : Int.Linear.Expr} {p : Int.Linear.Poly}
  {re : Lean.Meta.Grind.Arith.CommRing.RingExpr} {rp : Lean.Grind.CommRing.Poly} {p' : Int.Linear.Poly}
  {h_1 : Lean.Expr} {x_1 : Int.Linear.Var} {e'_1 : Int.Linear.Expr} {p_1 : Int.Linear.Poly}
  {re_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr} {rp_1 : Lean.Grind.CommRing.Poly} {p'_1 : Int.Linear.Poly},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing h x e' p re rp p' =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing h_1 x_1 e'_1 p_1 re_1 rp_1 p'_1 →
    h = h_1 ∧ x = x_1 ∧ e' = e'_1 ∧ p = p_1 ∧ re = re_1 ∧ rp = rp_1 ∧ p' = p'_1