proposition: Theorem app_imap_compose_x : forall I A B (f : A -> B) (x : A), ipure (f x) = imap f (@ipure _ _ I _ x).
proof: Proof. intros. assert (ipure (f x) = (@ipure _ _ I _ \o f) x). unfold comp. reflexivity. assert (imap f (ipure x) = (imap f \o @ipure _ _ I _) x). unfold comp. reflexivity. rewrite H0. rewrite H1. rewrite app_imap_compose. reflexivity. Qed.
imports: Hask.Ltac Hask.Prelude FunctionalExtensionality