proposition: Theorem binds_concat_ok_comm : forall A x (v : A) (F G : gen_env A), binds x v (F & G) -> ok (F & G) -> binds x v (G & F).
proof: Proof. intros A x v F G Hbind Hok. apply binds_concat_inv in Hbind. destruct Hbind as [ Hbind | [ Hnotin Hbind ] ]. assert (x ∈ G) by (apply binds_belongs with v; auto). assert (x ∉ F) by (apply belongs_ok_concat_inv_r with G; auto). apply binds_concat_l; auto. apply binds_concat_r; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv