Previously we saw how Refinement Reflection
can be used to write Haskell functions that prove theorems about
other Haskell functions. Today, we will see how Refinement Reflection
works on **recursive data types**.
As an example, we will prove that **lists are monoids** (under nil and append).

Lets see how to express **the monoid laws** as liquid types, and then prove
the laws by writing plain Haskell functions that are checked by LiquidHaskell.