Started typing for lemmas: Added ability to specify type signature for a...

Started typing for lemmas: Added ability to specify type signature for a lemmas variables (to become mandatory). If lemma eek is formulated 'Lemma eek: forall x :: a, y :: a : x .=. y', then we can't use the 'case analysis on x :: U'-trick, because it won't typecheck. We still have to check types when applying lemmas though.

Closes #73 (closed)