proposition: Lemma subvars_flat_map : forall A, forall f : A -> list NVar, forall l k, subvars (flat_map f l) k <=> forall x, LIn x l -> subvars (f x) k.
proof: Proof. intros. unfold subvars, sub_vars. repeat (trw subsetb_subset). trw subset_flat_map; split; sp. repeat (trw subsetb_subset). apply_hyp; sp. apply_in_hyp p. repeat (allrw subsetb_subset); auto. Qed.
imports: list Omega