since the df optim backward optim has been disabled, elimination is in a fixpoint now so elim chains are taken into account

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

Discussion w Xavier: replace this mechanism (fragile because of non-constructive witnesses) with a ghost-variables-based mechanism