environ
    given x,y being THING;
    A: P[x,y,x];
begin

               == Generalize with respect to y.
    ex a being THING st P[x,a,x] by A;                      == ExI

               == Generalize with respect to x.
    ex b being THING st P[b,y,b] by A;                      == ExI

               == Generalize with respect to the first x.
    ex c being THING st P[c,y,x] by A;                      == ExI

               == Generalize with respect to nothing.
    ex d being THING st P[x,y,x] by A;                      == ExI