fact: Definition ixapp_merge {X Y Z W} (f : X → Y) (g : Z → W) (t : X * Z) : Y * W := match t with (x, z) => (f x, g z) end.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple