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