Seeking uses of / functions that operate on “separated conjunction”

The Hasochism paper^^[PDF] defines two different conjunctions:

• Non-separating conjunction available in base Data.Functor.Product

    data Product :: (k -> Type) -> (k -> Type) -> (k -> Type) where
      Pair :: f a -> g a -> (Product f g) a
  

• The lesser known separated conjunction is the one I am interested in

    data (:**:) :: (a -> Type) -> (b -> Type) -> ((a, b) -> Type) where
      (:&&:) :: f a -> g b -> (f :**: g) '(a, b)
  

It also introduces the function wrapPair

data Ex :: (k -> Type) -> Type where
  Ex :: f xx -> Ex f

wrapPair :: (a -> Ex f) -> (b -> Ex g) -> ((a, b) -> Ex (f :**: g))
wrapPair f g (f***g -> (Ex x, Ex y)) = 
  Ex (x :&&: y)

Interested in all comments — in particular other names for these constructs, use cases, functions on them or any cool feedback