so now i’m curious, why not have == be guided by a protocol underneath that returns Substitutions? since goals are expected to return a stream of substitutions it seems like it doesn’t necessarily need to be limited to either the unit stream or nil.

iow you could have an implementation of == for maps such that it returns a goal which, if possible, produces a stream all of the possible substitutions.