proposition: Lemma list_inserts_0_l l1 l2 l3 : length l1 = length l3 → list_inserts 0 (l1 ++ l2) l3 = l1.
proof: Proof. revert l3. induction l1 as [|x l1 IH]; intros [|z l3] ?; simplify_eq/=. { by rewrite list_inserts_nil. } rewrite list_inserts_cons. simpl. by rewrite IH. Qed.
imports: stdpp(options)