proposition: Lemma lookup_insert_bingo: forall A x y (o : option A) e, x = y -> lookup x (raw_insert y o e) = o.
proof: Proof. induction x; intros; destruct y; destruct e; simpl; intuition; lia. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)