proposition: Theorem all_binds_concat_l : forall A (E F G : gen_env A), E ⊏ F -> (dom E) ⊄ G -> E ⊏ (F & G).
proof: Proof. intros A E F G Habind Hdom; unfold all_binds in *; intros x v Hbind. apply binds_concat_l; auto. apply binds_belongs in Hbind. auto. apply all_notin_def_inv with (dom E); auto. apply belongs_dom; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv