fact: Definition OmniscientT (O : Type) : Prop := forall p : O -> bool, (exists o : O, p o = false) \/ (forall o : O, p o = true).
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)