proposition: Lemma concat_replicate_is_iterated_insert: forall (A : Type) n (a : A) e, insert n a (concat e (replicate n a)) = concat e (replicate (S n) a).
proof: Proof. intros. simpl. eauto using insert_concat, length_replicate. Qed.
imports: List Dblib(DblibTactics DeBruijn)