entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner]
adapted the proof to show that the axiom of choice in equivalence
classes entails Excluded-Middle in Type Theory.
entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner]
adapted the proof to show that the axiom of choice in equivalence
classes entails Excluded-Middle in Type Theory.