[isabelle] remdups_adj crucial lemma

Hello everyone,

am I just bad at using find_theorems or is there no lemma that remdups_adj
really yields lists with no adjacent entries being equal? If it's really
missing, here's my somewhat lengthy proof:

Best regards

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