proposition: Lemma omniscient_dec (O A B : Type) (f : O -> A + B) : OmniscientT O -> surjective f -> inhabited A \/ ~ inhabited A.
proof: Proof. intros. pose (p := fun x => match f x with inl _ => false | inr _ => true end). specialize (H p) as [[o]|]. - left. unfold p in H. destruct (f o); auto; discriminate. - right. intros [a]. specialize (H0 (inl a)) as [o]. specialize (H o). unfold p in H. rewrite H0 in H. discriminate. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)