proposition: Lemma get_some : forall x E, x \in dom E -> exists v, get x E = Some v.
proof: Proof. Proof using. unfold binds. introv H. rew_env_defs. induction E as [|[y v] E']. rew_list in H. rewrite* in_empty in H. unfold get_impl. case_if. eauto. rew_listx in H. rewrite in_union in H. destruct H as [H|H]. rewrite in_singleton in H. simpls. false. forwards* [v' ?]: IHE'. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)