English
If q1 ∈ stmts₁ q₂, then membership propagates along step translation from q₂ to q₁.
Русский
Если q₁ ∈ stmts₁(q₂), тогда переходная индукция сохраняет принадлежность для q₁ по отношению к q₂.
LaTeX
$$stmts₁_trans (q₁) (q₂) ...$$
Lean4
theorem stmts_trans {M : Λ → Stmt Γ Λ σ} {S : Finset Λ} {q₁ q₂ : Stmt Γ Λ σ} (h₁ : q₁ ∈ stmts₁ q₂) :
some q₂ ∈ stmts M S → some q₁ ∈ stmts M S :=
by
simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq, forall_eq',
exists_imp, and_imp]
exact fun l ls h₂ ↦ ⟨_, ls, stmts₁_trans h₂ h₁⟩