finish port of modelset.ml

with the exception of UNION and SETUNION, which are claimed to be
unnecessary for the semantics.