(datatype Nat
    (Num i64)
    (OtherNum i64))



(rule ((= y 2))
      ((union (OtherNum y) (Num y))))

(Num 2)


(run 100)

(check (= (OtherNum 2) (Num 2)))