proposition: Theorem all_binds_ok_concat_inv : forall A (E F G : gen_env A), ok (E & F) -> (E & F) ⊏ G -> E ⊏ G ∧ F ⊏ G.
proof: Proof. intros A E F G Hok Habind; unfold all_binds in *. split; intros x v Hbind; apply Habind. apply binds_concat_l; auto. apply binds_belongs in Hbind. apply belongs_ok_concat_inv_l with E; auto. apply binds_concat_r; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv