proposition: Theorem all_binds_l_concat : forall A (E F G : gen_env A), E ⊏ G -> F ⊏ G -> (E & F) ⊏ G.
proof: Proof. intros. unfold all_binds in *. intros x v Hbind. apply binds_concat_inv in Hbind. destruct Hbind as [ Hbind | [ Hnotin Hbind] ]; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv