pub fn decide_nmset_subtraction(
    ctx: &Ctx,
    ns1: NmSet,
    ns2: NmSet
) -> Result<IdxTm, Error>
Expand description

Tactic to find an index term j such that NmSet(ns1) == NmSet(ns2) % j