proposition: Lemma dom_push : forall x v E, dom (E & x ~ v) = \{x} \u dom E.
proof: Proof. Proof using. intros. rewrite dom_concat. rewrite dom_single. rewrite~ union_comm. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)