proposition: Lemma lookup_map_some: forall A B x a e (f : A -> B), lookup x e = Some a -> lookup x (map f e) = Some (f a).
proof: Proof. induction x; intros; destruct e as [ | [ | ] ? ]; simpl in *; subst; try solve [ congruence | eauto ]. Qed.
imports: List Dblib(DblibTactics DeBruijn)