[STATEMENT]
lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x = y) = (rev (to_bl x) = rev (to_bl y))
[PROOF STEP]
by simp