MoreStlc.v done.
MoreStlc.v, added "soundness"
Typechecking.v done.