proposition: Theorem update_is_remove_concat : forall A x (v : A) (E : gen_env A), x ∈ E -> E ::= (x ∶ v) ≍ (E ∖ {x}) & (x ∶ v).
proof: Proof. intros A x v E Hin. unfold eq. split; unfold all_binds; intros y w Hbind. apply binds_update_inv in Hbind. destruct Hbind as [ [ Hnotin Hbind ] | [ Hin2 Hbind ] ]. apply binds_concat_l; auto. apply notin_single_inv in Hnotin. apply binds_remove; auto. apply binds_concat_r; auto. apply binds_concat_inv in Hbind. destruct Hbind as [ Hbind | [ Hnotin Hbind ] ]. apply binds_single_inv in Hbind. destruct Hbind; subst. apply binds_update_self; auto. apply binds_update_notin; auto. apply binds_remove_inv with x; auto. apply notin_single_inv with A v; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv