case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (Cont.then a✝ k')) a✝¹ = Cfg.then (stepNormal a✝² (Cont.cons₂ v a✝) a✝¹) k'

case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ stepNormal a✝¹ (Cont.then a✝ k') v = Cfg.then (stepNormal a✝¹ a✝ v) k'

case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ (if List.headI v = 0 then Cfg.then (stepRet a✝ (List.tail v)) k'
    else stepNormal a✝¹ (Cont.fix a✝¹ (Cont.then a✝ k')) (List.tail v)) =
    Cfg.then (if List.headI v = 0 then stepRet a✝ (List.tail v) else stepNormal a✝¹ (Cont.fix a✝¹ a✝) (List.tail v)) k'
k k' : Cont
v : List ℕ
⊢ stepRet (Cont.then k k') v = Cfg.then (stepRet k v) k'
induction k generalizing v <;> simp only [Cont.then, stepRet, *] <;>
  try { simp only [Cfg.then]; done }
case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ stepNormal a✝¹ (Cont.then a✝ k') v = Cfg.then (stepNormal a✝¹ a✝ v) k'

case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ (if List.headI v = 0 then Cfg.then (stepRet a✝ (List.tail v)) k'
    else stepNormal a✝¹ (Cont.fix a✝¹ (Cont.then a✝ k')) (List.tail v)) =
    Cfg.then (if List.headI v = 0 then stepRet a✝ (List.tail v) else stepNormal a✝¹ (Cont.fix a✝¹ a✝) (List.tail v)) k'
case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (Cont.then a✝ k')) a✝¹ = Cfg.then (stepNormal a✝² (Cont.cons₂ v a✝) a✝¹) k'

case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ stepNormal a✝¹ (Cont.then a✝ k') v = Cfg.then (stepNormal a✝¹ a✝ v) k'

case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ (if List.headI v = 0 then Cfg.then (stepRet a✝ (List.tail v)) k'
    else stepNormal a✝¹ (Cont.fix a✝¹ (Cont.then a✝ k')) (List.tail v)) =
    Cfg.then (if List.headI v = 0 then stepRet a✝ (List.tail v) else stepNormal a✝¹ (Cont.fix a✝¹ a✝) (List.tail v)) k'
case cons₁ =>
  rw [← stepNormal_then]
  rfl
case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ (if List.headI v = 0 then Cfg.then (stepRet a✝ (List.tail v)) k'
    else stepNormal a✝¹ (Cont.fix a✝¹ (Cont.then a✝ k')) (List.tail v)) =
    Cfg.then (if List.headI v = 0 then stepRet a✝ (List.tail v) else stepNormal a✝¹ (Cont.fix a✝¹ a✝) (List.tail v)) k'
case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ stepNormal a✝¹ (Cont.then a✝ k') v = Cfg.then (stepNormal a✝¹ a✝ v) k'

case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ (if List.headI v = 0 then Cfg.then (stepRet a✝ (List.tail v)) k'
    else stepNormal a✝¹ (Cont.fix a✝¹ (Cont.then a✝ k')) (List.tail v)) =
    Cfg.then (if List.headI v = 0 then stepRet a✝ (List.tail v) else stepNormal a✝¹ (Cont.fix a✝¹ a✝) (List.tail v)) k'
case comp =>
  rw [← stepNormal_then]
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (Cont.then a✝ k')) a✝¹ = stepNormal a✝² (Cont.then (Cont.cons₂ v a✝) k') a✝¹
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (Cont.then a✝ k')) a✝¹ = Cfg.then (stepNormal a✝² (Cont.cons₂ v a✝) a✝¹) k'
rw [← stepNormal_then]
no goals
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (Cont.then a✝ k')) a✝¹ = stepNormal a✝² (Cont.then (Cont.cons₂ v a✝) k') a✝¹
rfl
no goals
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ stepNormal a✝¹ (Cont.then a✝ k') v = Cfg.then (stepNormal a✝¹ a✝ v) k'
rw [← stepNormal_then]
case inl
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
h✝ : List.headI v = 0
⊢ Cfg.then (stepRet a✝ (List.tail v)) k' = Cfg.then (stepRet a✝ (List.tail v)) k'

case inr
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
h✝ : ¬List.headI v = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (Cont.then a✝ k')) (List.tail v) =
    Cfg.then (stepNormal a✝¹ (Cont.fix a✝¹ a✝) (List.tail v)) k'
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
⊢ (if List.headI v = 0 then Cfg.then (stepRet a✝ (List.tail v)) k'
    else stepNormal a✝¹ (Cont.fix a✝¹ (Cont.then a✝ k')) (List.tail v)) =
    Cfg.then (if List.headI v = 0 then stepRet a✝ (List.tail v) else stepNormal a✝¹ (Cont.fix a✝¹ a✝) (List.tail v)) k'
split_ifs
no goals
case inl
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
h✝ : List.headI v = 0
⊢ Cfg.then (stepRet a✝ (List.tail v)) k' = Cfg.then (stepRet a✝ (List.tail v)) k'
rw [← k_ih]
case inr
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
h✝ : ¬List.headI v = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (Cont.then a✝ k')) (List.tail v) =
    stepNormal a✝¹ (Cont.then (Cont.fix a✝¹ a✝) k') (List.tail v)
case inr
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
h✝ : ¬List.headI v = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (Cont.then a✝ k')) (List.tail v) =
    Cfg.then (stepNormal a✝¹ (Cont.fix a✝¹ a✝) (List.tail v)) k'
rw [← stepNormal_then]
no goals
case inr
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (Cont.then a✝ k') v = Cfg.then (stepRet a✝ v) k'
v : List ℕ
h✝ : ¬List.headI v = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (Cont.then a✝ k')) (List.tail v) =
    stepNormal a✝¹ (Cont.then (Cont.fix a✝¹ a✝) k') (List.tail v)
rfl