proposition: Lemma map_seq_app start xs1 xs2 : map_seq start (xs1 ++ xs2) =@{M A} map_seq start xs1 ∪ map_seq (start + length xs1) xs2.
proof: Proof. revert start. induction xs1 as [|x1 xs1 IH]; intros start; simpl. - by rewrite (left_id_L _ _), Nat.add_0_r. - by rewrite IH, Nat.add_succ_r, !insert_union_singleton_l, (assoc_L _). Qed.
imports: Coq(Permutation) stdpp(options)