[STATEMENT]
lemma path_append_elim[elim!] :
  assumes "path M q (p1@p2)"
  obtains "path M q p1"
      and "path M (target q p1) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>path M q p1; path M (target q p1) p2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms path_prefix path_suffix)