proposition: Lemma binds_middle_eq_inv : forall x E1 E2 v1 v2, binds x v1 (E1 & x ~ v2 & E2) -> ok (E1 & x ~ v2 & E2) -> v1 = v2.
proof: Proof. Proof using. introv H O. lets [? ?]: ok_middle_inv O. forwards~ M: binds_concat_left_inv H. applys~ binds_push_eq_inv M. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)