use ghost variables instead of existential variables to avoid read / write capture problems with variable reuse
use ghost variables instead of existential variables to avoid read / write capture problems with variable reuse