case comp
k' : Cont
v✝ : List ℕ
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, eval (then a✝ k') v = eval a✝ v >>= eval k'
v : List ℕ
⊢ Code.eval a✝¹ v >>= eval (then a✝ k') = Code.eval a✝¹ v >>= fun x => eval a✝ x >>= eval k'

case fix
k' : Cont
v✝ : List ℕ
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, eval (then a✝ k') v = eval a✝ v >>= eval k'
v : List ℕ
⊢ (if List.headI v = 0 then eval a✝ (List.tail v) >>= eval k'
    else Code.eval (Code.fix a✝¹) (List.tail v) >>= eval (then a✝ k')) =
    (if List.headI v = 0 then eval a✝ (List.tail v) else Code.eval (Code.fix a✝¹) (List.tail v) >>= eval a✝) >>= eval k'
k k' : Cont
v : List ℕ
⊢ eval (then k k') v = eval k v >>= eval k'
induction' k with _ _ _ _ _ _ _ _ _ k_ih _ _ k_ih generalizing v <;>
  simp only [Cont.eval, Cont.then, bind_assoc, pure_bind, *]
no goals
case comp
k' : Cont
v✝ : List ℕ
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, eval (then a✝ k') v = eval a✝ v >>= eval k'
v : List ℕ
⊢ Code.eval a✝¹ v >>= eval (then a✝ k') = Code.eval a✝¹ v >>= fun x => eval a✝ x >>= eval k'
simp only [← k_ih]
no goals
case fix
k' : Cont
v✝ : List ℕ
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, eval (then a✝ k') v = eval a✝ v >>= eval k'
v : List ℕ
⊢ (if List.headI v = 0 then eval a✝ (List.tail v) >>= eval k'
    else Code.eval (Code.fix a✝¹) (List.tail v) >>= eval (then a✝ k')) =
    (if List.headI v = 0 then eval a✝ (List.tail v) else Code.eval (Code.fix a✝¹) (List.tail v) >>= eval a✝) >>= eval k'
split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]