proposition: Lemma Foo_Algebra : forall a b, Foo a b ≅ (a * b) + (a * a * Foo a b) + unit.
proof: Proof. intros. exists (fun f => match f with | mkFoo a b => inl (inl (a, b)) | mkBar a1 a2 r => inl (inr (a1, a2, r)) | mkBaz => inr tt end). exists (fun p => match p with | inl (inl (a, b)) => mkFoo _ _ a b | inl (inr (a1, a2, r)) => mkBar _ _ a1 a2 r | inr tt => mkBaz _ _ 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 Hask.Data.Functor.Fix Hask.Control.Monad.Freer