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

State before:
cs : List (Thunk × List Bool)
x✝³ x✝² : Thunk
x✝¹ x✝ : List (Thunk × List Bool)
⊢ step^[0] (execution x✝³ x✝¹) = execution x✝² x✝ → step^[0] (execution x✝³ (x✝¹ ++ cs)) = execution x✝² (x✝ ++ cs)
Tactic:
simp
State after:
no goals