theorem ex₂ : ∀ (x₁ x₂ x₃ x₄ : Nat), x₁ + x₂ + (x₃ + x₄) = x₃ + x₁ + x₂ + x₄ :=
fun x₁ x₂ x₃ x₄ =>
  Expr.eq_of_sort_flat
    { op := Nat.add, assoc := Nat.add_assoc, comm := Nat.add_comm, vars := [x₁, x₂, x₃, x₄], someVal := x₁ }
    (((Expr.var 0).op (Expr.var 1)).op ((Expr.var 2).op (Expr.var 3)))
    ((((Expr.var 2).op (Expr.var 0)).op (Expr.var 1)).op (Expr.var 3)) rfl