proposition: Theorem all_belongs_all_binds : forall A xs (F : gen_env A), xs ⊂ F -> exists vs, (xs ∷ vs) ⊏ F.
proof: Proof. induction xs as [ | x xs IHxs ]; intros F Hin. exists nil; rewrite singles_empty; apply all_binds_empty_l; auto. apply all_belongs_belongs in Hin. destruct Hin as [ Hxin Hxsin ]. apply IHxs in Hxsin. destruct Hxsin as [ vs Habind ]. apply belongs_binds in Hxin. destruct Hxin as [ v Hbind ]. exists (v :: vs). rewrite singles_cons. unfold all_binds. intros y w Hbind2. apply binds_concat_inv in Hbind2. destruct Hbind2 as [ Hbind2 | [ Hnotin Hbind2 ] ]. apply binds_single_inv in Hbind2. destruct Hbind2; subst; auto. unfold all_binds in Habind; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv