switch to sptrees instead of num |-> unit

because this enables removing comparison of HOL sets, which won't
translate

proofs not updated