pub fn decide_nmset_subtraction( ctx: &Ctx, ns1: NmSet, ns2: NmSet) -> Result<IdxTm, Error>
Tactic to find an index term j such that NmSet(ns1) == NmSet(ns2) % j
j
NmSet(ns1) == NmSet(ns2) % j