proposition: Lemma binds_middle_inv : forall x1 v1 x2 v2 E1 E2, binds x1 v1 (E1 & x2 ~ v2 & E2) -> (binds x1 v1 E2) \/ (x1 # E2 /\ x1 = x2 /\ v1 = v2) \/ (x1 # E2 /\ x1 <> x2 /\ binds x1 v1 E1).
proof: Proof. Proof using. introv H. lets [?|[? M]]: (binds_concat_inv H). left~. right. lets [N|[? N]]: (binds_concat_inv M). lets [? ?]: (binds_single_inv N). subst~. right. simpl_dom. split~. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)