REST: REwriting in SmT solvers Documentation The .pdf that explains REST is available here Using Liquid Haskell Tactics The code for the template Haskell proof generator is available here The Liquid Haskell fork that supports rewriting is available here Supplementary Material 7.1: Comparison 7.2: Inductive Proofs 7.3: Set Properties 7.3: List Properties 7.3: Tree Properties