proposition: Lemma get_some_inv : forall x v E, get x E = Some v -> x \in dom E.
proof: Proof. Proof using. unfold binds. introv H. rew_env_defs. unfolds get_impl. induction E as [|[y v'] E']. false. rew_listx. rewrite in_union. simpl. case_if. inverts H. subst. left. rewrite~ in_singleton. forwards*: IHE'. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)