proposition: Lemma remove_nvars_flat_map : forall T, forall f : T -> list NVar, forall l : list T, forall vars : list NVar, remove_nvars vars (flat_map f l) = flat_map (compose (fun vs => remove_nvars vars vs) f) l.
proof: Proof. induction l; simpl; sp. apply remove_nvars_nil_r. rewrite remove_nvars_app_r. rewrite IHl. unfold compose. auto. Qed.
imports: list Omega