proposition: Lemma take_insert l n i x : n ≤ i → take n (<[i:=x]>l) = take n l.
proof: Proof. intros. apply list_eq. intros j. destruct (le_lt_dec n j). - by rewrite !lookup_take_ge. - by rewrite !lookup_take, !list_lookup_insert_ne by lia. Qed.
imports: stdpp(options)