proposition: Lemma lookup_shift_insert: forall A x y (o : option A) e, lookup (shift y x) (raw_insert y o e) = lookup x e.
proof: Proof. intros. destruct_lift_idx. - rewrite lookup_insert_old by lia. f_equal. lia. - rewrite lookup_insert_recent by lia. reflexivity. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)