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