proposition: Lemma binds_empty_inv : forall x v, binds x v empty -> False.
proof: Proof. Proof using. unfold binds. introv H. rewrite get_empty in H. false. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)