proposition: Lemma singles_keys_values : forall E, E = keys E ~* values E.
proof: Proof. Proof using. intros. rew_env_defs. induction E as [|[x v] E']. auto. rew_listx. simpl. rew_env_defs. rew_listx. fequals. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)