Hi List, Lukas Bulwahn discovered that the above lemma is inconsistently named. It should be set_takeWhileD without the underscore, since all other lemmas and the function "takeWhile" is named like that. Any objections to the renaming? Alex