[isabelle] Fw : Re: Question on hypothesis

how to do when I have a conjunction of hypothesis to simplify 
I have tried :
theory Scratch
  imports Main
have "(i+length l2=iP+length l2P) & (l1 @ l2=l1P @ l2P) & (l2P=[]) & (length l1+length l2=length l1P+length l2P)"  apply simp
but it doesn't work.
Best Regards.

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