phase splitting the lemmas.
Merge branch 'master' of github.com:jesper-bengtson/MirrorCharge
proof for the canceller.

- still need to come up with a proof for the
  simple ordering heuristic.