funext x'
case e_a.h.e_a
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
x' : a
⊢ (fun r2 => do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (r2 :: __do_lift)) =
    fun b => do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

case e_a.h.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
x' : a
⊢ ∀ {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
case e_a.h.e_a.h
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
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (x' :: bs)

case e_a.h.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
x' : a
⊢ ∀ {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