[STATEMENT]
lemma \<G>_semantics':
  "\<G> \<phi> w = subformulas\<^sub>\<nu> \<phi> \<inter> {\<psi>. w \<Turnstile>\<^sub>n G\<^sub>n \<psi>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<G> \<phi> w = subformulas\<^sub>\<nu> \<phi> \<inter> {\<psi>. w \<Turnstile>\<^sub>n G\<^sub>n \<psi>}
[PROOF STEP]
unfolding \<G>_semantics
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<psi> \<in> subformulas\<^sub>\<nu> \<phi>. w \<Turnstile>\<^sub>n G\<^sub>n \<psi>} = subformulas\<^sub>\<nu> \<phi> \<inter> {\<psi>. w \<Turnstile>\<^sub>n G\<^sub>n \<psi>}
[PROOF STEP]
by auto