proposition: Lemma ok_singles : forall n E xs (vs:list A), fresh (dom E) n xs -> length xs = length vs -> ok E -> ok (E & xs ~* vs).
proof: Proof. Proof using. introv F EQ O. gen E n vs. induction xs; destruct vs; destruct n; intros; tryfalse. rewrite singles_nil. rewrite~ concat_empty_r. rew_list in EQ. inverts EQ. simpl in F. destruct F as [Fr F']. lets [? M]: (fresh_union_r F'). rewrite singles_cons. rewrite concat_assoc. applys ok_push. applys~ IHxs n. simpl_dom. rewrite~ dom_singles. lets~: fresh_single_notin M. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)