fact: Example FiniteT_impl_OmniscientT (X : Type) : FiniteT X -> OmniscientT X.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)