bedrock2 does not consider pairs of lists to be valid cmds

[JasonGross]

#887 added translation support for pairs, but did not update the validity function. @jadephilipoom how should the validity condition be updated (should it be split into "valid anywhere" (expr), "valid at top-level" (let), and "valid in output" (list and pair)? or should it just be updated with pairs?).

Also, should the synthesis binaries check the validity of the bedrock2 they generate?

[andres-erbsen]

Clarification from meeting: the validity conditions are about PHOAS->bedrock2 translator input, not output. Currently the translator proof passes because the validity precondition is too strict.