Coq: SF Sub - typing substitution lemma
Coq: SF Sub - typing substitution lemma

Finally finished the proof!  Some code cleanup, most importantly all
unnecessary typing inversion lemmas for fix were removed.

jstolarek/sandbox,jstolarek/sandbox,jstolarek/sandbox