proposition: Lemma map_push : forall f x v E, map f (E & x ~ v) = map f E & x ~ f v.
proof: Proof. Proof using. intros. rewrite map_concat, map_single. auto. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)