Started work on porting this branch to the new version of Charge!.
Added axiom of functional choice which is needed to prove the frame rule
for receive.
Merge branch 'fangel' of https://git@github.com/jesper-bengtson/Java.git
into fangel

Conflicts:
	Java/src/Java/Semantics/SemCmd.v