[STATEMENT]
theorem app_eq: "app xs ys zs = (zs = xs @ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app xs ys zs = (zs = xs @ ys)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. app xs ys zs \<Longrightarrow> zs = xs @ ys
 2. zs = xs @ ys \<Longrightarrow> app xs ys zs
[PROOF STEP]
apply (erule app_eq2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zs = xs @ ys \<Longrightarrow> app xs ys zs
[PROOF STEP]
apply (erule app_eq1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done