proposition: Theorem eq_concat_comm : forall A (E F : gen_env A), ok (E & F) -> (E & F) ≍ (F & E).
proof: Proof. intros. unfold eq. split; apply all_binds_concat_ok_comm; auto. auto; apply all_binds_refl; auto. apply all_binds_refl; auto. apply ok_concat_comm; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv