proposition: Lemma binds_fresh_inv : forall x v E, binds x v E -> x # E -> False.
proof: Proof. Proof using. introv H F. unfolds binds. induction E as [|E' x' v'] using env_ind. rewrite get_empty in H. false. rewrite get_push in H. case_if~. subst. simpl_dom; notin_false. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)