proposition: Theorem ixfun_composition_x : forall {I O X Y Z} (f : Y -> Z) (g : X -> Y) (x : F I O X), f <$$> (g <$$> x) = (f \o g) <$$> x.
proof: Proof. intros. rewrite <- ixfun_composition. reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple