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; intuition; try lia. - erewrite <- lookup_empty_None. intuition. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)