fact: Definition ixapp_prod `{IxApplicative T F} {I J K X Y} (x : F I J X) (y : F J K Y) : F I K (X * Y)%type := pair <$$> x <**> y.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple