proposition: Lemma binds_single_inv : forall x1 x2 v1 v2, binds x1 v1 (x2 ~ v2) -> x1 = x2 /\ v1 = v2.
proof: Proof. Proof using. unfold binds. introv H. rewrite get_single in H. case_if; inversions~ H. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)