Completed alloc lemma. This commits includes failed lemmas (which are not in use).
Cleanup after alloc proof. Alloc QED.
Added swap example. This commits contains several attempts at the read rule.
Merged.