proposition: Lemma insert_concat_replicate: forall (A : Type) n x nx (a : option A) (b : A) e1, n + x = nx -> raw_insert nx a (concat e1 (replicate n b)) = concat (raw_insert x a e1) (replicate n b).
proof: Proof. eauto using insert_concat, length_replicate. Qed.
imports: List Dblib(DblibTactics DeBruijn)