proposition: Lemma map_insert: forall A B (f : A -> B) x a e, map f (insert x a e) = insert x (f a) (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 Dblib(DblibTactics DeBruijn)