-
Robbert Krebbers authored
This is allowed as long as one of the conjuncts is thrown away (i.e. is a wildcard _ in the introduction pattern). It corresponds to the principle of "external choice" in linear logic.
1c0a0e04
This is allowed as long as one of the conjuncts is thrown away (i.e. is a wildcard _ in the introduction pattern). It corresponds to the principle of "external choice" in linear logic.