[STATEMENT]
lemma boxed_b_eq_eq:
  assumes  "boxed_b \<Theta> n1 b1 bv b' n1'" and "boxed_b \<Theta> n2 b1 bv b' n2'" and "s = SBool (n1 = n2)" and  "\<turnstile>\<^sub>w\<^sub>f \<Theta>"
    "s' = SBool (n1' = n2')"
  shows  "s=s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using boxed_b_eq assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?\<Theta>  \<turnstile> ?s1.0 ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s1' ;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta> ;    \<turnstile>\<^sub>w\<^sub>f ?\<Theta> ;  ?\<Theta>  \<turnstile> ?s2.0 ~ ?b [ ?bv ::= ?b' ] \<setminus> ?s2' \<rbrakk> \<Longrightarrow> (?s1.0 = ?s2.0) = (?s1' = ?s2')
 \<Theta>  \<turnstile> n1 ~ b1 [ bv ::= b' ] \<setminus> n1'
 \<Theta>  \<turnstile> n2 ~ b1 [ bv ::= b' ] \<setminus> n2'
s = SBool (n1 = n2)
   \<turnstile>\<^sub>w\<^sub>f \<Theta>
s' = SBool (n1' = n2')

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by auto