proposition: Lemma insert_map_seq_0 xs i x: i < length xs → <[i:=x]> (map_seq 0 xs) =@{M A} map_seq 0 (<[i:=x]> xs).
proof: Proof. intros. rewrite insert_map_seq by lia. auto with f_equal lia. Qed.
imports: Coq(Permutation) stdpp(options)