Berardi.vo ChoiceFacts.vo ClassicalChoice.vo ClassicalDescription.vo ClassicalEpsilon.vo ClassicalFacts.vo Classical_Pred_Type.vo Classical_Prop.vo ClassicalUniqueChoice.vo Classical.vo ConstructiveEpsilon.vo Decidable.vo Description.vo Diaconescu.vo Epsilon.vo Eqdep_dec.vo EqdepFacts.vo Eqdep.vo WeakFan.vo WKL.vo FunctionalExtensionality.vo ExtensionalityFacts.vo Hurkens.vo IndefiniteDescription.vo JMeq.vo ProofIrrelevanceFacts.vo ProofIrrelevance.vo RelationalChoice.vo SetIsType.vo FinFun.vo