proposition: Lemma fv_in_values_binds : forall y fv x v E, binds x v E -> y \notin fv_in_values fv E -> y \notin fv v.
proof: Proof. Proof using. unfold fv_in_values. introv H. induction E using env_ind; introv M. false. applys* binds_empty_inv. rewrite values_def in M,IHE. rewrite concat_def, single_def in M. rew_listx in M. simpl in M. lets [[? ?]|[? ?]]: (binds_push_inv H); subst~. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)