proposition: Theorem eq_all_belongs : forall A xs (E F : gen_env A), E ≍ F -> xs ⊂ E -> xs ⊂ F.
proof: Proof. intros A xs E F Heq Hin. unfold eq in *. destruct Heq as [ Habind1 Habind2 ]. apply all_binds_belongs in Habind1. apply all_belongs_def. intros. apply all_belongs_def_inv with (dom E); auto. apply belongs_dom. apply all_belongs_def_inv with xs; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv