[STATEMENT]
lemma release_and_right_distrib:
  "w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi>\<^sub>1 and\<^sub>n \<psi>\<^sub>2) \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> R\<^sub>n \<psi>\<^sub>1) and\<^sub>n (\<phi> R\<^sub>n \<psi>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi>\<^sub>1 and\<^sub>n \<psi>\<^sub>2) = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi>\<^sub>1 and\<^sub>n \<phi> R\<^sub>n \<psi>\<^sub>2
[PROOF STEP]
by auto