proposition: Lemma insert_map_seq start xs i x: start ≤ i < start + length xs → <[i:=x]> (map_seq start xs) =@{M A} map_seq start (<[i - start:=x]> xs).
proof: Proof. intros. apply map_eq. intros j. destruct (decide (i = j)) as [->|?]. - rewrite lookup_insert, lookup_map_seq, option_guard_True by lia. by rewrite list_lookup_insert by lia. - rewrite lookup_insert_ne, !lookup_map_seq by done. case_guard; [|done]. by rewrite list_lookup_insert_ne by lia. Qed.
imports: Coq(Permutation) stdpp(options)