proposition: Lemma insert_insert_always: forall A k s (a b : option A) e, raw_insert k a (raw_insert s b e) = raw_insert (shift k s) b (raw_insert (if le_gt_dec k s then k else k - 1) a e).
proof: Proof. intros. destruct (le_gt_dec k s). rewrite lift_idx_old by assumption. eauto using insert_insert. rewrite lift_idx_recent by assumption. replace k with (1 + (k - 1)) in * by omega. rewrite <- insert_insert by omega. do 2 f_equal. omega. Qed.
imports: List Dblib(DblibTactics DeBruijn)