case zero'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal Code.zero' k v = Cfg.ret k' v'

case succ
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal Code.succ k v = Cfg.ret k' v'

case tail
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal Code.tail k v = Cfg.ret k' v'

case cons
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.cons a✝¹ a✝) k v = Cfg.ret k' v'

case comp
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.comp a✝¹ a✝) k v = Cfg.ret k' v'

case case
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.case a✝¹ a✝) k v = Cfg.ret k' v'

case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
c : Code
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal c k v = Cfg.ret k' v'
induction c generalizing k v
case cons
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.cons a✝¹ a✝) k v = Cfg.ret k' v'

case comp
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.comp a✝¹ a✝) k v = Cfg.ret k' v'

case case
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.case a✝¹ a✝) k v = Cfg.ret k' v'

case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
case zero'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal Code.zero' k v = Cfg.ret k' v'

case succ
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal Code.succ k v = Cfg.ret k' v'

case tail
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal Code.tail k v = Cfg.ret k' v'

case cons
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.cons a✝¹ a✝) k v = Cfg.ret k' v'

case comp
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.comp a✝¹ a✝) k v = Cfg.ret k' v'

case case
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.case a✝¹ a✝) k v = Cfg.ret k' v'

case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
iterate 3 exact ⟨_, _, rfl⟩
case comp
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.comp a✝¹ a✝) k v = Cfg.ret k' v'

case case
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.case a✝¹ a✝) k v = Cfg.ret k' v'

case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
case cons
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.cons a✝¹ a✝) k v = Cfg.ret k' v'

case comp
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.comp a✝¹ a✝) k v = Cfg.ret k' v'

case case
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.case a✝¹ a✝) k v = Cfg.ret k' v'

case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
case cons _f fs IHf _IHfs => apply IHf
case case
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.case a✝¹ a✝) k v = Cfg.ret k' v'

case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
case comp
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.comp a✝¹ a✝) k v = Cfg.ret k' v'

case case
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.case a✝¹ a✝) k v = Cfg.ret k' v'

case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
case comp f _g _IHf IHg => apply IHg
case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
case case
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.case a✝¹ a✝) k v = Cfg.ret k' v'

case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
case case f g IHf IHg =>
  rw [stepNormal]
  simp only []
  cases v.headI <;> simp only [] <;> [apply IHf; apply IHg]
no goals
case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
case fix f IHf => apply IHf
case cons
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.cons a✝¹ a✝) k v = Cfg.ret k' v'

case comp
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.comp a✝¹ a✝) k v = Cfg.ret k' v'

case case
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.case a✝¹ a✝) k v = Cfg.ret k' v'

case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
case tail
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal Code.tail k v = Cfg.ret k' v'

case cons
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.cons a✝¹ a✝) k v = Cfg.ret k' v'

case comp
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.comp a✝¹ a✝) k v = Cfg.ret k' v'

case case
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝¹ k v = Cfg.ret k' v'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.case a✝¹ a✝) k v = Cfg.ret k' v'

case fix
a✝ : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal a✝ k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix a✝) k v = Cfg.ret k' v'
exact ⟨_, _, rfl⟩
no goals
_f fs : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal _f k v = Cfg.ret k' v'
_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal fs k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.cons _f fs) k v = Cfg.ret k' v'
apply IHf
no goals
f _g : Code
_IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal _g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.comp f _g) k v = Cfg.ret k' v'
apply IHg
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v',
    (fun k v => Nat.rec (stepNormal f k (List.tail v)) (fun y x => stepNormal g k (y :: List.tail v)) (List.headI v)) k
        v =
      Cfg.ret k' v'
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.case f g) k v = Cfg.ret k' v'
rw [stepNormal]
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v',
    Nat.rec (stepNormal f k (List.tail v)) (fun y x => stepNormal g k (y :: List.tail v)) (List.headI v) = Cfg.ret k' v'
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v',
    (fun k v => Nat.rec (stepNormal f k (List.tail v)) (fun y x => stepNormal g k (y :: List.tail v)) (List.headI v)) k
        v =
      Cfg.ret k' v'
simp only []
no goals
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v',
    Nat.rec (stepNormal f k (List.tail v)) (fun y x => stepNormal g k (y :: List.tail v)) (List.headI v) = Cfg.ret k' v'
cases v.headI <;> simp only [] <;> [apply IHf; apply IHg]
no goals
f : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (Code.fix f) k v = Cfg.ret k' v'
apply IHf