Remove environments from star/plus/etc.
Towards compcomp: remove big step semantics.
Towards compcomp: remove backward simulation, interpreter, behaviors.

These should be replaced by something suitable in the future.
Decouple memories.
Prove that each semantics is "forward".
Remove duplicate Forall2 notions.