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.