wandIntro : All (p ^*^ q :-> r) -> All (p :-> q ~* r)
wandIntro f pl = \sp, qr => f $ MkStar pl sp qr

wandCancel0 : All (p :-> q ~* r) -> All (p ^*^ q :-> r)
wandCancel0 f (MkStar pl sp qr) = f pl sp qr

wandCancel : All $ p ^*^ (p ~* q) :-> q
wandCancel (MkStar pl sp wr) = wr (splitComm sp) pl

wandMono : All (p :-> q) -> All (r :-> s) -> All (q ~* r :-> p ~* s)
wandMono pq rs wqr = \sp, pr => rs $ wqr sp (pq pr)

wandSelf : All $ Emp :-> p ~* p
wandSelf MkEmp = \sp, pr => rewrite splitRInv sp in pr

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

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

wandStar : All $ (p ~* q) ^*^ r :-> p ~* (q ^*^ r)
wandStar (MkStar pql sp1 rr) = \sp2, pr =>
  let (_ ** (sp3, sp4)) = splitUnassoc (splitComm sp2) sp1 in
  MkStar (pql (splitComm sp3) pr) sp4 rr