proposition: Lemma binds_push_inv : forall x1 v1 x2 v2 E, binds x1 v1 (E & x2 ~ v2) -> (x1 = x2 /\ v1 = v2) \/ (x1 <> x2 /\ binds x1 v1 E).
proof: Proof. Proof using. introv H. unfolds binds. rewrite get_push in H. case_if. inverts~ H. auto. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)