proposition: Theorem exp_add_iso : forall a b c, ((a + b) -> c) -> c ≅ (a -> c) -> (b -> c) -> c.
proof: Proof. intros. exists (fun k l r => k (fun p => match p with | inl x => l x | inr x => r x end)). exists (fun k p => k (fun a => p (inl a)) (fun a => p (inr a))). extensionalize. f_equal. extensionality p. destruct p; trivial. 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