proposition: Theorem all_binds_concat_compat : forall A (E F G : gen_env A), E ⊏ F -> (E & G) ⊏ (F & G).
proof: Proof. intros A E F G Habind. induction G using env_ind. rewrite ?concat_empty_r; auto. unfold all_binds. intros y w Hbind. rewrite concat_assoc in *. apply binds_concat_inv in Hbind. destruct Hbind as [ Hbind | [ Hnotin Hbind ] ]. apply binds_concat_r; auto. apply binds_concat_l; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv