add wp proof rule for recursive functions

This is just added for demonstration purposes, and so that when we show it in papers (or a PhD thesis ;), we can rightfully claim it has been mechanized.