update lec-refinement-types-2.markdown

Ranjit, let me know if you want me to change something.

Also, I observed that the well-formedness rules are not explicitly used in the typing rules, 
so I added an invariant for the environment gamma that types should be well-formed.