proposition: Lemma FooF_Algebra : forall a b r, FooF a b r ≅ (a * b) + (a * a * r) + unit.
proof: Proof. intros. exists (fun f => match f with | mkFooF a b => inl (inl (a, b)) | mkBarF a1 a2 r => inl (inr (a1, a2, r)) | mkBazF => inr tt end). exists (fun p => match p with | inl (inl (a, b)) => mkFooF _ _ _ a b | inl (inr (a1, a2, r)) => mkBarF _ _ _ a1 a2 r | inr tt => mkBazF _ _ _ 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