Added SfLib dependency, and created a gitignore for Coq-generated files.
Defined step up to primitives. Added examples.

We have defined plus and provided some examples of stepping through a
simple program. We still need to work on defining evaluation contexts
however, so we can't evaluate more complex examples (as demonstrated by
the admit towards the end.)