improved some comments in core defs file, and added fvar substitution for contexts
proved some stuff about source contexts; still a little stuck on one lemma