proposition: Theorem all_binds_update_self : forall A (E F : gen_env A), (dom E) ⊂ F -> E ⊏ (F ::= E).
proof: Proof. intros A E F Hdom. unfold all_binds. intros x v Hbind. induction E as [ | E y w IHE ] using env_ind. apply binds_empty in Hbind. inversion Hbind. rewrite dom_concat in Hdom. rewrite dom_single in Hdom. simpl in Hdom. apply all_belongs_belongs in Hdom. destruct Hdom as [ Hin Hdom ]. apply binds_concat_inv in Hbind. rewrite update_concat_r. destruct Hbind as [ Hbind | [ Hnotin Hbind ] ]. apply binds_single_inv in Hbind. destruct Hbind; subst. apply binds_update_self. apply belongs_update; auto. apply notin_single_inv in Hnotin. rewrite update_update_one. apply binds_update_one_neq; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv