Theorem: HMem.Stack.step_execution_append (HMem/Program/Step.lean)

State before:
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)
Tactic:
cases t₀ with | _ m c p => cases c <;> cases cs₀ <;> simp [List.append_left_inj]
State after:
no goals

State before:
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)
Tactic:
cases c <;> cases cs₀ <;> simp [List.append_left_inj]
State after:
no goals