Description: Version of eu3v where the disjoint variable condition is replaced with
a nonfreeness hypothesis. This is a "backup" of a theorem that used to
be in the main part with label "eu3" and was deprecated in favor of
eu3v . (Contributed by NM, 8-Jul-1994)(Proof shortened by BJ, 31-May-2019)