proposition: Lemma insert_take_drop l i x : i < length l → <[i:=x]> l = take i l ++ x :: drop (S i) l.
proof: Proof. intros Hi. rewrite <-(take_drop_middle (<[i:=x]> l) i x). 2:{ by rewrite list_lookup_insert. } rewrite take_insert by done. rewrite drop_insert_gt by lia. done. Qed.
imports: stdpp(options)