[STATEMENT]
lemma interleave_cont_rev_conc[simp]: "b@a \<in> a\<otimes>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b @ a \<in> a \<otimes> b
[PROOF STEP]
apply (subgoal_tac "b@a \<in> b\<otimes>a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b @ a \<in> b \<otimes> a \<Longrightarrow> b @ a \<in> a \<otimes> b
 2. b @ a \<in> b \<otimes> a
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b @ a \<in> b \<otimes> a
[PROOF STEP]
apply(simp only: interleave_cont_conc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done