Lessness (Mar 14 2023 at 20:03): Lessness (Mar 14 2023 at 20:03):In the theories/ordinals/Schutte/Countable.v file of hydra-battles, there is an ad-hoc formalization of countable Prop-based sets. The question is "is there already such a formalization in the Coq libraries ?"
(from PM by Pierre Castéran)
Is this task important/good right now? If yes, I'm going to take a look at this file and then explore if there's some library that does the same job...
Last updated: Jun 10 2023 at 23:01 UTC