proposition: Theorem all_binds_concat_ok_comm : forall A (E F G : gen_env A), E ⊏ (F & G) -> ok (F & G) -> E ⊏ (G & F).
proof: Proof. intros. unfold all_binds in *. intros. apply binds_concat_ok_comm; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv