1 theory Chap03

     2 theory Chap03

     2 imports Main

     3 imports Main

     3 begin

     4 begin

     4 

     5 

     5 lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"

     6 lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"