[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:
https://gist.github.com/javra/68c7f852a060d7cb6036

Best regards
Jakob



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