proposition: Lemma map_singles : forall (f : A -> B) xs vs, length xs = length vs -> map f (xs ~* vs) = xs ~* (LibList.map f vs).
proof: Proof. Proof using. intros. rew_env_defs. gen vs. induction xs; destruct vs; introv E; tryfalse. rew_list~. rew_listx. simpl. rew_list. fequals~. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)