  (.) = inNew2 $ \ g f -> \ a -> let f' = f a
                                     g' = g (copoint f')
                                 in
                                   g' . f'

#if 0

type OkCart k = OpCon (Prod k) (Sat (Ok (Local k)))

instance OpCon (:*) (Sat (Ok k)) => OpCon (:*) (Sat (OkLocal k)) where
  inOp :: (Sat (OkLocal k) a, Sat (OkLocal k) b) |- Sat (OkLocal k) (a :* b)
  inOp = Entail (Sub Dict) -- <+ okProd @k @a @b

-- Could not deduce (Copointed (k (a, b)))