Added typable_empty_closed;
Lemma says, if something typed in an empty context, it has no free variables.