proposition: Lemma map_concat : forall f E F, map f (E & F) = map f E & map f F.
proof: Proof. Proof using. intros. rew_env_defs. gen E. induction F as [|(x,v)]; intros. rew_listx~. rew_listx. fequals. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)