(datatype Math
  (Num Rational)
  (Var String)
  (Add Math Math)
  (Div Math Math)
  (Mul Math Math))

(let z (Var "z"))

(Add (Var "x") (Var "y"))

(rewrite (Add a z) a)

(run 2)

(fail (check (= (Var "x") (Add (Var "x") (Var "y")))))