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.
Edited by Robbert Krebbers