case nil
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
⊢ List.bind ([] ++ ys) f = List.bind [] f ++ List.bind ys f

case cons
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : List.bind (tail✝ ++ ys) f = List.bind tail✝ f ++ List.bind ys f
⊢ List.bind (head✝ :: tail✝ ++ ys) f = List.bind (head✝ :: tail✝) f ++ List.bind ys f
α : Type u_1
β : Type u_2
xs ys : List α
f : α → List β
⊢ List.bind (xs ++ ys) f = List.bind xs f ++ List.bind ys f
induction xs
case cons
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : List.bind (tail✝ ++ ys) f = List.bind tail✝ f ++ List.bind ys f
⊢ List.bind (head✝ :: tail✝ ++ ys) f = List.bind (head✝ :: tail✝) f ++ List.bind ys f
case nil
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
⊢ List.bind ([] ++ ys) f = List.bind [] f ++ List.bind ys f

case cons
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : List.bind (tail✝ ++ ys) f = List.bind tail✝ f ++ List.bind ys f
⊢ List.bind (head✝ :: tail✝ ++ ys) f = List.bind (head✝ :: tail✝) f ++ List.bind ys f
{rfl}
no goals
case cons
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : List.bind (tail✝ ++ ys) f = List.bind tail✝ f ++ List.bind ys f
⊢ List.bind (head✝ :: tail✝ ++ ys) f = List.bind (head✝ :: tail✝) f ++ List.bind ys f
simp_all [cons_bind, append_assoc]