Classical logic

I propose to add an stdlib file for basic classical reasoning.

This does NOT mean assuming excluded middle, of course, but rather defining what it is, and proving some characterizations.