Fix muxing of datatype constructor values.
Fix muxing of datatype constructor values.

This really only properly handles pretty narrow situations regarding
constructors. Muxing data type values will only succeed if the same
constructor is used in both values, and if the constructor forms
a non-dependent function on its regular (non-parameter) arguments.
However, this is similar to the prior situation, where the constructors
were required to be the same, and muxing arguments would panic if
they differed in shape.

GaloisInc/saw-script,GaloisInc/saw-script,GaloisInc/saw-script,GaloisInc/saw-script,GaloisInc/saw-script