proposition: Lemma submseteq_insert l1 l2 i j x y : l1 !! i = Some x → l2 !! j = Some x → l1 ⊆+ l2 → (<[i := y]> l1) ⊆+ (<[j := y]> l2).
proof: Proof. intros ?? Hsub. rewrite !insert_take_drop, <-!Permutation_middle by eauto using lookup_lt_Some. rewrite <-(take_drop_middle l1 i x), <-(take_drop_middle l2 j x), <-!Permutation_middle in Hsub by done. by apply submseteq_skip, (submseteq_app_inv_l _ _ [x]). Qed.
imports: stdpp(options)