proposition: Lemma dom_concat : forall E F, dom (E & F) = dom E \u dom F.
proof: Proof. Proof using. intros. rew_env_defs. gen E. induction F as [|(x,v)]; intros. rew_listx. rewrite~ union_empty_r. rew_listx. simpl. rewrite IHF. rewrite~ union_comm_assoc. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)