Prove simple list head

This will be the last example done in simple-untyped. I will start proving examples in KernelC.
Yeah, I can do that. But I decided to write it this way because it is closer to the MatchC specification style, namely ```$ => return Y:Int```. Besides, since SIMPLE do not do garbage collection, I will have to write an additional ```.Map => ?M:Map``` in the ```store``` cell. 

Should I write the function specification in this function call style in the future?