proposition: Theorem ixapp_identity_x : ∀ {I X} {x : F I I X}, ixap (ixpure (@id X)) x = id x.
proof: Proof. intros. rewrite app_ixmap_unit. apply ixfun_identity_x. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple