[STATEMENT]
lemma append_eq_cong: "\<lbrakk>eq xs ys; eq xs' ys'\<rbrakk> \<Longrightarrow> eq (xs @ xs') (ys @ ys')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivclp cancel1 xs ys; equivclp cancel1 xs' ys'\<rbrakk> \<Longrightarrow> equivclp cancel1 (xs @ xs') (ys @ ys')
[PROOF STEP]
by(induction rule: equivclp_induct)(auto intro: eq_append_same1 equivclp_into_equivclp cancel1_append_same2)