proposition: Lemma Foo_FooF_eq : forall a b x, Foo_to_FooF a b (FooF_to_Foo a b x) = x.
proof: Proof. intros. extensionality r. extensionality h. Admitted. Lemma Foo_Fix_FooF : forall a b, Foo a b ≅ Fix (FooF a b). Proof. intros. exists (Foo_to_FooF a b). exists (FooF_to_Foo a b). unfold comp. split; extensionality x. exact (Foo_FooF_eq a b x). exact (FooF_Foo_eq a b x). 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