proposition: Lemma binds_concat_left_ok : forall x v E1 E2, ok (E1 & E2) -> binds x v E1 -> binds x v (E1 & E2).
proof: Proof. Proof using. introv O H. induction E2 using env_ind. rewrite~ concat_empty_r. rewrite concat_assoc in O|-*. lets [_ ?]: ok_push_inv O. applys~ binds_push_neq. intro_subst. applys~ binds_fresh_inv H. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)