Add lemmas `elem_of_prefix` and `elem_of_suffix`

Added a lemma that captures that any element [x] that is in a prefix [l1] is also in the full list [l2]. The property is only trivial from the definition of l1 prefix_of l2 (i.e. ∃ l, l2 = l1 ++ l2). Adding the lemma thus avoids breaking abstraction.

If you had the time to add the same lemma for suffix, that would be great. :) (but no big deal if not)

added 1 commit

• 47f70920 - Updated name/order to match existing lemmas and added suffix variant

Compare with previous version

added 1 commit

• 94befedc - Updated names of lemmas to be consistent with existing lemmas

Compare with previous version

resolved all threads

changed title from Added [prefix_elem_of] lemma to Add{+ lemmas elem_of_prefix and elem_of_suffix+}

Merging. Thanks!

merged

mentioned in commit f23a05c3