proposition: Lemma binds_concat_left : forall x v E1 E2, binds x v E1 -> x # E2 -> binds x v (E1 & E2).
proof: Proof. Proof using. introv H F. induction E2 using env_ind. rewrite~ concat_empty_r. rewrite concat_assoc. applys~ binds_push_neq. simpl_dom. auto. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)