spark2014/include

More details about adding lemmas to the SPARK lemma library are found in the
internal wiki. The basic information is the following.

* To rebuild everything from scratch (make a save of sessions/proofs if needed) use:
     source setup.sh
     generate_session.py
  If this fails, try removing obj and sessions first:
     rm -rf obj/
     rm -rf proof/sessions/
     generate_session.py

  If this still fails (it should not), try increasing the levels in generate_session.py.
  If this comes from a Coq proof, try to find it in proof/Coq/common.

* When you add a manual proof, please add the corresponding check in manual.in.
  Check that this is buildable with generate_session.py

* To regenerate automatically .ctx from .v (generated by why3) you just have to
  use generate_session.py by replacing the call to diff_all(False) by
  diff_all(True)