proposition: Lemma dom_map : forall (B:Type) (f:A->B) E, dom (map f E) = dom E.
proof: Proof. Proof using. induction E using env_ind. rewrite map_empty. do 2 rewrite dom_empty. auto. rewrite map_concat. rewrite map_single. rewrite_all dom_concat. rewrite_all dom_single. congruence. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)