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.
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.