proposition: Lemma elem_of_list_split_length l i x : l !! i = Some x → ∃ l1 l2, l = l1 ++ x :: l2 ∧ i = length l1.
proof: Proof. revert i; induction l as [|y l IH]; intros [|i] Hl; simplify_eq/=. - exists []; eauto. - destruct (IH _ Hl) as (?&?&?&?); simplify_eq/=. eexists (y :: _); eauto. Qed.
imports: stdpp(options)