This implements an ifEx (x1, x2, ...) (phi) (t1) (t2) operator.
The meaning of this expression is given by
(ifEx (x1, x2, ...) (phi) (t1) (t2)) equiv (ifEx (x1) (ex x2. ... phi) (ifEx (x2, ...) (phi) (t1) (t2)) (t2))
and by
(ifEx (x1) (phi) (t1) (t2)) equiv (if (ex x1. phi) ({x1 (min x1. phi)}t1) (t2))