proposition: Lemma binds_concat_right : forall x v E1 E2, binds x v E2 -> binds x v (E1 & E2).
proof: Proof. Proof using. introv H. induction E2 using env_ind. false. applys* binds_empty_inv. rewrite concat_assoc. lets [[? ?]|[? ?]]: binds_push_inv H. subst. applys binds_tail. applys~ binds_push_neq. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)