proposition: Lemma map_keys_push : forall r x v E, map_keys r (E & x ~ v) = map_keys r E & r x ~ v.
proof: Proof. Proof using. intros. rewrite map_keys_concat, map_keys_single. auto. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)