∀ (lhs rhs lhs' rhs' : Lean.Meta.Grind.Arith.CommRing.RingExpr) (vars : Array Lean.Expr)
  (lhs_1 rhs_1 lhs'_1 rhs'_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr) (vars_1 : Array Lean.Expr),
  ({ lhs := lhs, rhs := rhs, lhs' := lhs', rhs' := rhs', vars := vars } =
      { lhs := lhs_1, rhs := rhs_1, lhs' := lhs'_1, rhs' := rhs'_1, vars := vars_1 }) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ lhs' = lhs'_1 ∧ rhs' = rhs'_1 ∧ vars = vars_1)