proposition: Lemma map_keys_concat : forall r E F, map_keys r (E & F) = map_keys r E & map_keys r 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)