environ
    given Fred being PERSON;
    given Hello being STATEMENT;

    A1: for x being PERSON holds
           ex s being STATEMENT st 
             (Tells[x,s] & Tells[x,Hello] & s <> Hello & True[s]);
begin
          == Here we universally instantiate, substituting Fred for x
          == and eliminating the universal quantifier.
1: ex s being STATEMENT st
     (Tells[Fred,s] & Tells[Fred,Hello] & s <> Hello & True[s]) by A1; == UE

          == Existential generalization, replace all occurrences
          == of Hello by t, and add the existential quantifier
2: ex t being STATEMENT st
     ex s being STATEMENT st
       (Tells[Fred,s] & Tells[Fred,t] & s <> t & True[s]) by 1;        == ExI

          == Existentially generalize, replace only the first
          == of Fred occurrences by y, and add the existential quantifier.
3: ex y being PERSON st
     ex t being STATEMENT st
       ex s being STATEMENT st
         (Tells[y,s] & Tells[Fred,t] & s <> t & True[s]) by 2;         == ExI