Rohan Jacob-Rao, Andrew Cave, Brigitte Pientka: Mechanizing Proofs about Mendler-style Recursion. LFMTP 2016: 1:1-1:9