diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-18 20:39:34 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-24 12:25:55 +0200 |
| commit | e8e994afb5a29f92c750fb370d01b704ddf06cc4 (patch) | |
| tree | b971d0e9083c049c5fd0058bf316c4972589744a /theories/Sets/Powerset_Classical_facts.v | |
| parent | 2739fe8a22a9df48e717583d6efabc42e41f9814 (diff) | |
A new version of Hurkens.v.
Adds a more generic and modular proof of Hurkens, where a shallow embedding of U- is given in the most general way. Subsumes all the previous proofs, opens the way to new proofs.
Diffstat (limited to 'theories/Sets/Powerset_Classical_facts.v')
0 files changed, 0 insertions, 0 deletions