Theory Substitution_Sema

theory Substitution_Sema
imports Substitution Sema
begin

lemma substitution_lemma: "𝒜 ⊨ F[G / n] ⟷ 𝒜(n := 𝒜 ⊨ G) ⊨ F" by(induction F; simp)

end