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