proposition: Lemma exp_ex_iso : forall A (P : A -> Prop) (r : Prop), (exists x : A, P x) -> r ≅ (forall x : A, P x -> r).
proof: Proof. intros. exists (fun p x H => p (ex_intro _ x H)). exists (fun (k : forall x : A, P x -> r) p => match p with ex_intro x H => k x H end). extensionalize. Qed.
imports: Hask.Ltac Hask.Prelude Hask.Control.Applicative Hask.Control.Monad Hask.Control.Monad.Cont Hask.Control.Monad.State Hask.Data.Functor.Contravariant Hask.Data.Functor.Identity Hask.Data.Functor.Kan Hask.Data.Functor.Yoneda Hask.Control.Lens Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Init.Datatypes Coq.Relations.Relation_Definitions FunctionalExtensionality