[STATEMENT]
lemma distinct_mid_unique2: "\<lbrakk>distinct (xs@U@ys); U\<noteq>[]; xs@U@ys = as@U@bs\<rbrakk> \<Longrightarrow> ys = bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (xs @ U @ ys); U \<noteq> []; xs @ U @ ys = as @ U @ bs\<rbrakk> \<Longrightarrow> ys = bs
[PROOF STEP]
using distinct_mid_unique1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (?xs @ ?U @ ?ys); ?U \<noteq> []; ?xs @ ?U @ ?ys = ?as @ ?U @ ?bs\<rbrakk> \<Longrightarrow> ?as = ?xs

goal (1 subgoal):
 1. \<lbrakk>distinct (xs @ U @ ys); U \<noteq> []; xs @ U @ ys = as @ U @ bs\<rbrakk> \<Longrightarrow> ys = bs
[PROOF STEP]
by blast