[STATEMENT]
lemma en_eq_4[PLM]:
    "[(\<lbrace>x,F\<rbrace> \<^bold>\<equiv> \<lbrace>y,G\<rbrace>) \<^bold>\<equiv> (\<^bold>\<box>\<lbrace>x,F\<rbrace> \<^bold>\<equiv> \<^bold>\<box>\<lbrace>y,G\<rbrace>) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<lbrace>x,F\<rbrace> \<^bold>\<equiv> \<lbrace>y,G\<rbrace> \<^bold>\<equiv> (\<^bold>\<box>\<lbrace>x,F\<rbrace> \<^bold>\<equiv> \<^bold>\<box>\<lbrace>y,G\<rbrace>) in v]
[PROOF STEP]
by (metis CP en_eq_2 "\<^bold>\<equiv>I" "\<^bold>\<equiv>E"(1) "\<^bold>\<equiv>E"(2))