proposition: Lemma lookup_insert_old: forall A x y (o : option A) e, x > y -> lookup x (raw_insert y o e) = lookup (x - 1) e.
proof: Proof. induction x; intros; [ elimtype False; omega | replace (S x - 1) with x by omega ]. destruct y; destruct e; simpl; try solve [ eauto ]. rewrite lookup_empty_None. erewrite <- lookup_empty_None. eauto with omega. destruct x; intros; [ elimtype False; omega | replace (S x - 1) with x in * by omega ]. simpl lookup at 2. eauto with omega. Qed.
imports: List Dblib(DblibTactics DeBruijn)