proposition: Theorem binds_concat_r : forall A x (v : A) (F G : gen_env A), x ∹ v ⋲ G -> x ∹ v ⋲ (F & G).
proof: Proof. intros A x v F G Hbind. induction G as [ | G y w IHG ] using env_ind. apply binds_empty in Hbind. inversion Hbind. destruct (eq_keys_dec x y) as [ Heq | Hneq ]. rewrite <- Heq in *; clear y Heq. unfold binds in *. apply get_concat_inv in Hbind. destruct Hbind as [ [ _ Heq ] | [ Hneq Hbind ] ]. rewrite Heq in *. rewrite concat_assoc. apply get_concat_r; auto. elim Hneq; auto. unfold binds in *. rewrite concat_assoc. apply get_concat_inv in Hbind. destruct Hbind as [ [ Heq _ ] | [ _ Hget ] ]. contradiction. apply IHG in Hget. 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