cases t₀ with | _ m c p => cases c <;> cases cs₀ <;> simp [List.append_left_inj]
t₀ : Thunk
cs₀ : List (Thunk × List Bool)
t₁ : Thunk
cs₁ cs : List (Thunk × List Bool)
⊢ step (execution t₀ cs₀) = execution t₁ cs₁ → step (execution t₀ (cs₀ ++ cs)) = execution t₁ (cs₁ ++ cs)
no goals