This module implements the generation of equational theorems, given unfolding theorems. The unfolding theorems are generated differently for different kinds of recursive definition, but the code here is no longer cares about that.