proposition: Lemma binds_single_eq_inv : forall x v1 v2, binds x v1 (x ~ v2) -> v1 = v2.
proof: Proof. Proof using. introv H. unfolds binds. rewrite get_single in H. case_if. inverts~ H. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)