English
If q1 ∈ stmts1(q2) and S supports q2, then S supports q1.
Русский
Если q1 ∈ stmts1(q2) и S поддерживает q2, то S поддерживает q1.
LaTeX
$$$ q_1 \in stmts_1(q_2) \land SupportsStmt S\; q_2 \Rightarrow SupportsStmt S\; q_1 $$$
Lean4
theorem stmts₁_supportsStmt_mono {S : Finset Λ} {q₁ q₂ : Stmt Γ Λ σ} (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂) :
SupportsStmt S q₁ := by
induction q₂ with simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h hs
| branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
| goto l => subst h; exact hs
| halt => subst h; trivial
| load _ _ IH
| _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]