case cons head tail IH => {
  rewrite [mapM_cons];
  simp[fish];
  simp [bind_assoc]
  simp[mapM_cons];
  congr; funext x';
  rewrite [commute_implies_mapM_commute];
  congr;
  funext x';
  simp [fish] at IH;
  rewrite [<- IH];
  simp[bind_assoc];
  apply COMMUTE;
}
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) = mapM (fish f g) (head :: tail)
no goals