Monday meeting changes #1

 * Fixed semantics (audit the check rules)
 * Fixed names of thms/lems/defs and changed lems to props in sec 2