curryW : All $ (p ^*^ q) ~* r :-> p ~* (q ~* r)
curryW wpq_r =
  MkWand $ \sp1, pm =>
  MkWand $ \sp2, qr =>
  let (_ ** (sp3, sp4)) = splitAssoc sp1 sp2 in
  app wpq_r sp3 (MkStar pm sp4 qr)

uncurryW : All $ p ~* (q ~* r) :-> (p ^*^ q) ~* r
uncurryW wpqr = MkWand $ \sp1, (MkStar pl sp2 qr) =>
  let (_ ** (sp3, sp4)) = splitUnassoc sp1 sp2 in
  app (app wpqr sp3 pl) sp4 qr

curryW : All $ (p ^*^ q) ~* r :-> p ~* (q ~* r)
curryW wpq_r =
  MkWand $ \sp1, pm =>
  MkWand $ \sp2, qr =>
  let (_ ** (sp3, sp4)) = splitAssoc sp1 sp2 in
  app wpq_r sp3 (MkStar pm sp4 qr)

uncurryW : All $ p ~* (q ~* r) :-> (p ^*^ q) ~* r
uncurryW wpqr = MkWand $ \sp1, (MkStar pl sp2 qr) =>
  let (_ ** (sp3, sp4)) = splitUnassoc sp1 sp2 in
  app (app wpqr sp3 pl) sp4 qr