function subst(array &$old,$new) {
		if (is_string($new))
			$new=[$new];
		foreach ($new as $hdr) {
			$old=preg_grep('/'.preg_quote(strstr($hdr,':',TRUE),'/').':.+/',
				$old,PREG_GREP_INVERT);
			array_push($old,$hdr);
		}
	}