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