proposition: Corollary N_infty_omniscient : OmniscientT N_infty.
proof: Proof. red; intros Q. apply N_infty_omniscient'. intros. apply N_infty_extensionality in H. subst. reflexivity. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)