no goals
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
S : Finset Λ
k : K
s : StAct k
q : Stmt₂
⊢ TM2.SupportsStmt S (stRun s q) ↔ TM2.SupportsStmt S q
cases s <;> rfl