Fix typo (eqpath->eqtermalg)
Added universe annotation to El
Added universe annotation to nProd
Added universe annotation to nPrEqual and nJuEqual
Added universe annotation to coerce
With universe annotations, path equivalence works