prove constrained interpretation is still well-formed

needed to add a condition on the constraints as described in previous
commit