[isabelle] proof solution [ newbie question ]

I've been experimenting with the Isabelle prover and have reached a point in
a proof where I have the following subgoal:

/\ xs ys zs. [| hd xs = hd ys; tl xs @ zs = tl ys |] ==> xs @ zs = ys

This looks obvious to me (since xs @ zs = ys is equivalent to hd xs # tl xs
@ zs = hd ys # tl ys for non-empty xs) , but I don't know how to proceed.

Any suggestions?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.