proposition: Lemma binds_not_middle_inv : forall x v E1 E2 E3, binds x v (E1 & E2 & E3) -> x # E2 -> (binds x v E3) \/ (x # E3 /\ binds x v E1).
proof: Proof. Proof using. introv H F. lets [?|[? M]]: (binds_concat_inv H). left~. right. forwards~ N: (binds_concat_left_inv M). Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)