Creates a function and a macro to replace case-match, and prevent excessive casesplitting when proving lemmas.
