This is specially important. You are trying to use a const variable as it was a C macro, you want that any reference to that token/name is replaced by the code in the right-hand side in any context. This would never work. You can use a macro to do this replacement for you in a restrict scope and ∀ will need to be :∀ (probably).
2 Likes