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.