proposition: Lemma vlookup_insert_ne {A n} i j x (v : vec A n) : i ≠ j → vinsert i x v !!! j = v !!! j.
proof: Proof. induction i as [|?? IHi]; inv_fin j; inv_vec v; simpl; try done. intros. apply IHi. congruence. Qed.
imports: stdpp(countable) stdpp(options)