cases c <;> cases cs₀ <;> simp [List.append_left_inj]
case mk
cs₀ : List (Thunk × List Bool)
t₁ : Thunk
cs₁ cs : List (Thunk × List Bool)
m : Memory
c p : Program
⊢ step (execution { state := m, current := c, function := p } cs₀) = execution t₁ cs₁ →
    step (execution { state := m, current := c, function := p } (cs₀ ++ cs)) = execution t₁ (cs₁ ++ cs)
no goals