diff --git a/rest-rewrite.cabal b/rest-rewrite.cabal
--- a/rest-rewrite.cabal
+++ b/rest-rewrite.cabal
@@ -1,14 +1,19 @@
 name:               rest-rewrite
 build-type:         Simple
-version:            0.1
+version:            0.1.1
 cabal-version:      1.22
 category:           Rewriting
 maintainer:         Zack Grannan <zgrannan@cs.ubc.ca>
+author:             Zack Grannan <zgrannan@cs.ubc.ca>
 license:            BSD3
 description:        Rewriting library with online termination checking.
 synopsis:           Rewriting library with online termination checking
 license-file:       LICENSE
 
+source-repository head
+  type:     git
+  location: https://github.com/zgrannan/rest
+
 library
   default-language:  Haskell2010
   exposed-modules:
@@ -99,6 +104,7 @@
     OpOrdering
     QuickCheckTests
     RPO
+    Set
     StrictOC
     WQO
 
@@ -124,11 +130,13 @@
   other-modules:
       Arith
       BagExample
+      Compiler
       DSL
       Group
       Language.REST.AbstractOC
       Language.REST.ConcreteOC
       Language.REST.Core
+      Language.REST.Dot
       Language.REST.EquivalenceClass
       Language.REST.ExploredTerms
       Language.REST.MetaTerm
@@ -143,23 +151,23 @@
       Language.REST.OrderingConstraints.Strict
       Language.REST.PartialOrder
       Language.REST.Path
+      Language.REST.ProofGen
+      Language.REST.RESTDot
       Language.REST.RPO
       Language.REST.Rest
       Language.REST.Rewrite
       Language.REST.RewriteRule
       Language.REST.RuntimeTerm
+      Language.REST.SMT
       Language.REST.Types
-      Language.REST.WorkStrategy
       Language.REST.WQO
-      Language.REST.SMT
-      Compiler
+      Language.REST.WorkStrategy
       Lists
       Multiset
       MultisetOrdering
       Nat
       NonTerm
+      Set
       WQODot
-      Language.REST.Dot
-      Language.REST.RESTDot
 
   hs-source-dirs: src
diff --git a/src/Language/REST/ProofGen.hs b/src/Language/REST/ProofGen.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/REST/ProofGen.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Language.REST.ProofGen where
+
+import qualified Data.HashMap.Strict as M
+import qualified Data.List as L
+import qualified Data.Text as T
+import Text.Printf
+
+import Language.REST.Path
+import Language.REST.Rewrite
+import Language.REST.RuntimeTerm
+import Language.REST.Op
+
+-- Hardcoded
+opToLH (Op "union") = "mp"
+opToLH (Op "toMS")  = "multiset_of"
+opToLH (Op op) = T.unpack op
+
+withParens True t = "(" ++ t ++ ")"
+withParens False t = t
+
+toLH :: Bool -> RuntimeTerm -> String
+-- Hardcoded rules
+toLH parens (App "m" [arg]) = withParens parens $ printf "Multiset [%s]" (toLH False arg)
+toLH parens (App "cons" [x, xs]) = withParens parens $ printf "%s:%s" (toLH True x) (toLH True xs)
+
+toLH _ (App op [])   = opToLH op
+toLH parens (App op args) =
+  withParens parens $ printf "%s %s" (opToLH op) (L.intercalate " " $ map (toLH True) args)
+
+toProof :: Path Rewrite RuntimeTerm a -> String
+toProof (steps, PathTerm result _) = "    " ++ (L.intercalate "\n=== " $ proofSteps ++ [toLH False result]) ++ "\n*** QED"
+  where
+    proofSteps :: [String]
+    proofSteps = map proofStep $ zip steps [0..]
+
+    proofStep ((Step (PathTerm t _) _ _ True), _)     = toLH False t
+    proofStep ((Step (PathTerm t _) (Rewrite lhs rhs name) _ False), i) = toLH False t ++ " ? " ++ toLemma lemma
+      where
+        lemma = go (subTerms t)
+
+        lemmaName =
+          case name of
+            Just n  -> T.pack n
+            Nothing -> "lemma"
+
+        toLemma s = toLH False (App (Op lemmaName) (map snd $ L.sort $ M.toList s))
+
+        go []            = undefined
+        go ((st, f): _) | Just su <- unify lhs st M.empty
+                        , f (subst su rhs) == nextTerm
+                        = su
+        go (_:xs)       = go xs
+
+        nextTerm = if i < (length steps - 1) then (pathTerm . term) (steps !! (i + 1)) else result
diff --git a/src/Set.hs b/src/Set.hs
new file mode 100644
--- /dev/null
+++ b/src/Set.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Set where
+
+import Arith as A
+import Data.Text
+import DSL
+import Language.REST.MetaTerm
+import Language.REST.Op
+
+import qualified Data.HashSet as S
+
+emptyset  = RWApp "∅" []
+
+x /\ y = RWApp "intersect" [x, y]
+x \/ y  = RWApp "union" [x, y]
+
+s0 = RWApp "s₀" []
+s1 = RWApp "s₁" []
+
+isSubset t1 t2 = t1 \/ t2 ~> t2
+
+userRWs = S.union A.evalRWs $ S.fromList $
+  [
+    distribL (/\) (\/)
+  , distribR (/\) (\/)
+  , distribL (\/) (/\)
+  , distribR (\/) (/\)
+  --   assocL (\/)
+  -- , assocL (/\)
+  , x /\ x        ~> x
+  , x \/ x        ~> x
+  , x \/ emptyset ~> x
+  -- , commutes (\/)
+  -- , commutes (/\)
+
+  -- Example 1
+  , s1 /\ s0      ~> emptyset
+
+  -- Example 2
+  -- , s0 \/ s1      ~> s0
+  ]
+
+evalRWs = S.union A.userRWs $ S.fromList --
+  [ RWApp "t2" [] ~> emptyset
+  , isSubset (RWApp "right1" []) (RWApp "right" [])
+  ]
+
+disjointExample  = "union(union(left, right1), union(left,right))"
+disjointExample2 = "union(left, union(right1, union(left,right)))"
+
+example1 = "f(intersect(union(s₀,s₁), s₀))"
+example2 = "f(union(intersect(s₀,s₁), s₀))"