proposition: Theorem eq_concat : forall A (E F G : gen_env A), E ≍ F -> (E & G) ≍ (F & G).
proof: Proof. unfold eq; intros A E F G Heq. destruct Heq. split; apply all_binds_concat_compat; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv