Berardi.vo PropExtensionalityFacts.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 ExtensionalFunctionRepresentative.vo Hurkens.vo IndefiniteDescription.vo JMeq.vo ProofIrrelevanceFacts.vo ProofIrrelevance.vo PropFacts.vo PropExtensionality.vo RelationalChoice.vo SetIsType.vo SetoidChoice.vo FinFun.vo