proposition: Lemma binds_push_eq_inv : forall x v1 v2 E, binds x v1 (E & x ~ v2) -> v1 = v2.
proof: Proof. Proof using. introv H. forwards [|]: binds_push_inv H; auto_false*. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)