proposition: Theorem ixfun_identity_x : forall {I O X} (x : F I O X), ixmap id x = id x.
proof: Proof. intros. rewrite ixfun_identity. reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple