proposition: Lemma list_lookup_insert_Some l i x j y : <[i:=x]>l !! j = Some y ↔ i = j ∧ x = y ∧ j < length l ∨ i ≠ j ∧ l !! j = Some y.
proof: Proof. destruct (decide (i = j)) as [->|]; [split|rewrite list_lookup_insert_ne by done; tauto]. - intros Hy. assert (j < length l). { rewrite <-(insert_length l j x); eauto using lookup_lt_Some. } rewrite list_lookup_insert in Hy by done; naive_solver. - intros [(?&?&?)|[??]]; rewrite ?list_lookup_insert; naive_solver. Qed.
imports: stdpp(options)