Proved Match case with (probably) over-complicated proof
Roughly looked through the rest of the cases, Letrec should be the only hard one left