Added a substitution lemma using a postulate
Finished the first case study
Updated .gitignore