.
├── Berardi.html
├── Berardi.v
├── ChoiceFacts.html
├── ChoiceFacts.v
├── ClassicalChoice.html
├── ClassicalChoice.v
├── ClassicalDescription.html
├── ClassicalDescription.v
├── ClassicalEpsilon.html
├── ClassicalEpsilon.v
├── ClassicalFacts.html
├── ClassicalFacts.v
├── Classical.html
├── Classical_Pred_Type.html
├── Classical_Pred_Type.v
├── Classical_Prop.html
├── Classical_Prop.v
├── ClassicalUniqueChoice.html
├── ClassicalUniqueChoice.v
├── Classical.v
├── ConstructiveEpsilon.html
├── ConstructiveEpsilon.v
├── Decidable.html
├── Decidable.v
├── Description.html
├── Description.v
├── Diaconescu.html
├── Diaconescu.v
├── Epsilon.html
├── Epsilon.v
├── Eqdep_dec.html
├── Eqdep_dec.v
├── EqdepFacts.html
├── EqdepFacts.v
├── Eqdep.html
├── Eqdep.v
├── ExtensionalFunctionRepresentative.html
├── ExtensionalFunctionRepresentative.v
├── ExtensionalityFacts.html
├── ExtensionalityFacts.v
├── FinFun.html
├── FinFun.v
├── FunctionalExtensionality.html
├── FunctionalExtensionality.v
├── Hurkens.html
├── Hurkens.v
├── IndefiniteDescription.html
├── IndefiniteDescription.v
├── index.html
├── JMeq.html
├── JMeq.v
├── ProofIrrelevanceFacts.html
├── ProofIrrelevanceFacts.v
├── ProofIrrelevance.html
├── ProofIrrelevance.v
├── PropExtensionalityFacts.html
├── PropExtensionalityFacts.v
├── PropExtensionality.html
├── PropExtensionality.v
├── PropFacts.html
├── PropFacts.v
├── RelationalChoice.html
├── RelationalChoice.v
├── SetIsType.html
├── SetIsType.v
├── SetoidChoice.html
├── SetoidChoice.v
├── StrictProp.html
├── StrictProp.v
├── WeakFan.html
├── WeakFan.v
├── WKL.html
└── WKL.v
tree v1.8.0 © 1996 - 2018 by Steve Baker and Thomas Moore
HTML output hacked and copyleft © 1998 by Francesc Rocher
JSON output hacked and copyleft © 2014 by Florian Sesser
Charsets / OS/2 support © 2001 by Kyosuke Tokoro