/theories/Logic/

• ../
• Berardi.v
• ChoiceFacts.v
• Classical.v
• ClassicalChoice.v
• ClassicalDescription.v
• ClassicalEpsilon.v
• ClassicalFacts.v
• ClassicalUniqueChoice.v
• Classical_Pred_Type.v
• Classical_Prop.v
• ConstructiveEpsilon.v
• Decidable.v
• Description.v
• Diaconescu.v
• Epsilon.v
• Eqdep.v
• EqdepFacts.v
• Eqdep_dec.v
• ExtensionalFunctionRepresentative.v
• ExtensionalityFacts.v
• FinFun.v
• FunctionalExtensionality.v
• Hurkens.v
• IndefiniteDescription.v
• JMeq.v
• ProofIrrelevance.v
• ProofIrrelevanceFacts.v
• PropExtensionality.v
• PropExtensionalityFacts.v
• PropFacts.v
• RelationalChoice.v
• SetIsType.v
• SetoidChoice.v
• WKL.v
• WeakFan.v