Incorparating feedback, simplifying proofs

* Added all but three feedback elements from Implementation feedback
part 2
  - Haven't eliminated ret or live yet:
     Ret and live have different semantics, however it is possible to
simulate ret with live by \lambda x. live x, but it might prove
difficult  in proofs and to talk about it
  - May be requiring more examples, however the word count at the moment
is 11725 and still need a conclusion
  - Haven't played around with exact layouts of the semantics figures
yet.

* Proofs and semantics
  - Removed the inpair: it was a complete semantics duplication
  - Changed all of the proofs so that they work
  - "Simplified" a number of proofs by using copious amounts of
automatic proofsearch: less understandable by cases, much more succinct,
more resilient to slight changes.

* Added a makefile to build some stuff