proposition: Lemma binds_concat_left_inv : forall x v E1 E2, binds x v (E1 & E2) -> x # E2 -> binds x v E1.
proof: Proof. Proof using. introv H F. lets~ [M|[? ?]]: binds_concat_inv H. false. applys~ binds_fresh_inv M. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)