proposition: Lemma insert_concat: forall (A : Type) n x nx (o : option A) e1 e2, length e2 = n -> n + x = nx -> raw_insert nx o (concat e1 e2) = concat (raw_insert x o e1) e2.
proof: Proof. induction n; intros; subst; destruct e2; simpl in *; try discriminate; auto. rewrite insert_insert by omega. erewrite <- (IHn (1 + x)) by first [ congruence | eauto ]. eauto with f_equal omega. Qed.
imports: List Dblib(DblibTactics DeBruijn)