proposition: Lemma insert_insert: forall A k s (a b : option A) e, k <= s -> raw_insert k a (raw_insert s b e) = raw_insert (1 + s) b (raw_insert k a e).
proof: Proof. intros ? k s. generalize s k; clear s k. induction s; intros. destruct k; [ | elimtype False; omega ]. reflexivity. destruct k. reflexivity. destruct e; replace (1 + S s) with (S (1 + s)) by omega; simpl; f_equal; eauto with omega. Qed.
imports: List Dblib(DblibTactics DeBruijn)