package coq-functions-in-zfc

This mostly repeats Guillaume Alexandre's contribution `zf', but in classical logic and with a different proof style. We start with a simple axiomatization of some flavor of ZFC (for example Werner's implementation of ZFC should provide a model). We develop some very basic things like pairs, functions, and a little bit about natural numbers, following the standard classical path.