Function is_weak_kvar_sort 

fn is_weak_kvar_sort(sort: &Sort) -> bool

NOTE(CK):

• Skips params (we don’t presently handle polymorphism, though even if we did, I’m not sure that we need to pass params to the weak kvars).
• Skips locs because we can’t encode those.
• Skips aliases: a projection can normalize to a unit sort at a call-site, while the weak kvar’s declaration would still encode it as an integer.
• Skips unit + unit adts because they otherwise get encoded as a 0 tuple to fixpoint because we use them in the args to a weak kvar, which we don’t want to do.