There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
violation of declaration-quantification duality
Consider the following two fragments:
_(assert \forall T x; p)
Assuming that T is a type not requiring initialization (e.g. \integer) I believe it should be a principle that these should be equivalent. Sadly, they're not; there are cases where the first verifies and the second does not.