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