string.split
simp
c a_1 ... a_n = c b_1 ... b_n
a_1 = b_1 /\ ... /\ a_n = b_n
to_unfold
simplify
simp*