Re: [Hol-info] [SPAM] Re: some questions about the proving process in HOL4

/\ (l = l1 ++ l2) > : proof > The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])" > have already been in assumption list, so I think it is natural to get > "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove >

[Hol-info] [SPAM] Re: some questions about the proving process in HOL4

[]". But I tried many times , I can't prove that. Could anyone prove it? Thanks! --Wish. -- next part -- An HTML attachment was scrubbed... ---------- Message: 4 Date: Tue, 15 Dec 2015 14:34:44 +1100 From: Ramana Kumar <ramana