proposition: Lemma binds_map : forall x v (f : A -> B) E, binds x v E -> binds x (f v) (map f E).
proof: Proof. Proof using. introv H. unfolds binds. rew_env_defs. induction E as [|[x' v'] E']; rew_listx; simpls. false. simpls. case_if~; rew_listx. inverts~ H. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)