proposition: Lemma map_raw_insert: forall A B (f : A -> B) x e, map f (raw_insert x None e) = raw_insert x None (map f e).
proof: Proof. induction x; intros; destruct e; simpl; eauto. - rewrite IHx. reflexivity. - match goal with o: option _ |- _ => destruct o end; f_equal; eauto. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)