[STATEMENT]
lemma conjug_concat_conjug: "xs \<sim> ys \<Longrightarrow> concat xs \<sim> concat ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<sim> ys \<Longrightarrow> concat xs \<sim> concat ys
[PROOF STEP]
unfolding conjugate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r s. r \<cdot> s = xs \<and> s \<cdot> r = ys \<Longrightarrow> \<exists>r s. r \<cdot> s = concat xs \<and> s \<cdot> r = concat ys
[PROOF STEP]
using concat_morph
[PROOF STATE]
proof (prove)
using this:
concat (?xs \<cdot> ?ys) = concat ?xs \<cdot> concat ?ys

goal (1 subgoal):
 1. \<exists>r s. r \<cdot> s = xs \<and> s \<cdot> r = ys \<Longrightarrow> \<exists>r s. r \<cdot> s = concat xs \<and> s \<cdot> r = concat ys
[PROOF STEP]
by metis