type-checking monadic signatures; changed syntax of formulas tto disambiguate some connectives and type operators; using == for prop. equalit, =!= for disequality, and ~ for prop. negation