proposition: Theorem all_binds_belongs : forall A (E F : gen_env A), E ⊏ F -> (dom E) ⊂ F.
proof: Proof. unfold all_binds. intros A E F Hyp. apply all_belongs_def. intros x Hin. apply belongs_dom_inv in Hin. apply belongs_binds in Hin. destruct Hin as [ v Hbind ]. apply Hyp in Hbind. apply binds_belongs with v; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv