proposition: Lemma keys_singles : forall xs vs, length xs = length vs -> keys (xs ~* vs) = xs.
proof: Proof. Proof using. intros. rew_env_defs. gen vs. induction xs; destruct vs; introv E; rew_list in E; tryfalse. rew_list~. simpl. rew_env_defs. rew_listx. fequals. rew_list in E. applys IHxs. inverts E. auto. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)