proposition: Lemma binds_concat_inv' : forall A, forall x (v:A) E1 E2, binds x v (E1 & E2) -> (x # E2 /\ binds x v E1) \/ (binds x v E2).
proof: Proof. Proof using. intros. forwards K: binds_concat_inv A H. destruct* K. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)