proposition: Theorem app_pmap_compose_x : ∀ J A B (f : A → B) (x : A), ixpure (f x) = ixmap f (@ixpure _ F _ J _ x).
proof: Proof. intros. assert (ixpure (f x) = (@ixpure _ F _ J _ \o f) x). unfold comp. reflexivity. assert (ixmap f (ixpure x) = (ixmap f \o @ixpure _ _ _ J _) x). unfold comp. reflexivity. rewrite H0. rewrite H1. rewrite app_pmap_compose. reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple