proposition: Lemma binds_concat_inv : forall x v E1 E2, binds x v (E1 & E2) -> (binds x v E2) \/ (x # E2 /\ binds x v E1).
proof: Proof. Proof using. introv H. induction E2 using env_ind. rewrite~ concat_empty_r in H. rewrite concat_assoc in H. forwards [[? ?]|[? M]]: binds_push_inv H. subst. left. apply binds_tail. forwards [?|[? ?]]: IHE2 M. left. applys~ binds_push_neq. right~. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)