K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type u_3
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
k : K
q : Stmt₂
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f))
      (update S k
        (match StAct.peek f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => List.tail (S k)))
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type u_3
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
k : K
q : Stmt₂
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f)) (update S k (stWrite v (S k) (StAct.peek f)))
unfold stWrite
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type u_3
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
k : K
q : Stmt₂
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S = TM2.stepAux q (stVar v (S k) (StAct.peek f)) S
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type u_3
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
k : K
q : Stmt₂
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f))
      (update S k
        (match StAct.peek f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => List.tail (S k)))
rw [Function.update_eq_self]
no goals
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type u_3
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
k : K
q : Stmt₂
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S = TM2.stepAux q (stVar v (S k) (StAct.peek f)) S
rfl