proposition: Theorem binds_concat_l : forall A x (v : A) (F G : gen_env A), x ∹ v ⋲ F -> x ∉ G -> x ∹ v ⋲ (F & G).
proof: Proof. intros A x v F G Hbind Hnotin. induction G as [ | G y w IHG ] using env_ind. rewrite concat_empty_r; auto. apply notin_concat_inv in Hnotin. destruct Hnotin as [ HnotinG Hnotin_y ]. apply IHG in HnotinG. apply notin_single_inv in Hnotin_y. unfold binds in *. rewrite concat_assoc. assert (get x (F & G & y ∶ w) = get x (F & G)) as Heq. apply get_concat_l; auto. rewrite Heq; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv