Introduced notion of variabled exists in context
Better way to check if a variable is free
Proofed free-in-context lemma
Some progress in preservation proof