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