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