(datatype Expr
  (Mul Expr Expr)
  (Var String)
  (Lit i64)
)

; Assume injectivity of Mul for unification
(rule ((= (Mul a b) (Mul c d)))
      ((union a c)
       (union b d)))

;; (relation False (i64))
; If any Literal make equal to something it can't be, false is derived
;(rule ((= (Lit i) (Lit j)) (!= i j))
;      ((False 0)))
(rule ((= (Lit i) (Mul a b)))
      ((panic "Literal cannot be equal to a product")))

(union (Mul (Var "a") (Var "a")) 
     (Mul (Lit 1) (Lit 2)))


(run 3)
(check (= (Var "a") (Lit 1)))
(check (= (Lit 2) (Lit 1)))
; (check (False 0)) ;; this should fail because we don't want prove false