no goals
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type u_4
inst✝¹ : Inhabited Λ
σ : Type u_3
inst✝ : Inhabited σ
k : K
s : StAct k
q : Stmt₂
⊢ trNormal (stRun s q) = goto fun x x => go k s q
cases s <;> rfl