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