simp[fish]
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ fish (mapM f) (mapM g) (head :: tail) = do
    let b ← fish f g head
    let bs ← mapM (fish f g) tail
    pure (b :: bs)
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ (do
      let x ← f head
      let x_1 ← mapM f tail
      let __do_lift ← g x
      let __do_lift_1 ← mapM g x_1
      pure (__do_lift :: __do_lift_1)) =
    do
    let x ← f head
    let b ← g x
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)