environ
    given Hello being STATEMENT;
    given Fred being PERSON;
                == Hello is a true statement.
Fact1: True[Hello];
                == Fred always lies.
Fact2: for s being STATEMENT holds Tells[Fred,s] implies not True[s];
                == Every person is either a Knight or a Knave, but not both.
Opp: for a being PERSON holds Knight[a] iff not Knave[a];
                == A person is a knight if and only if every statement
                == they say is true.
Veracity: for a being PERSON holds
             Knight[a] iff
                (for s being STATEMENT holds Tells[a,s] implies True[s]);
                == If at least one of the things you say is false
                == then everything you say is false.
Consistency: for a being PERSON holds 
              (ex s being STATEMENT st Tells[a,s] & not True[s]) implies
               (for s being STATEMENT holds Tells[a,s] implies not True[s]);
                == Every person says at least one thing.
Verbosity: for p being PERSON holds ex s being STATEMENT st Tells[p,s];
                == Some person says everything.
BlabberMouth: ex p being PERSON st for s being STATEMENT holds Tells[p,s];

begin

                == We demonstrate that there is some person who says Hello.
                == Use the fact that blabber mouth exists.
    consider blabber being PERSON such that
      1: for s being STATEMENT holds Tells[blabber,s]
                                           by BlabberMouth;         == ExE
                == Combine this with the fact that Hello is a statement.
      2: Tells[blabber, Hello] by 1;                                == UE
                == Now existentially generalize
    ex p being PERSON st Tells[p,Hello] by 2;                       == ExI

        == We prove that there exists some person p such that if they
        == are a knight then all statements are true.
        == This example should demonstrate to you that the scope of
        == an existential quantifier better not be a conditional,
        == if it is possible for the antecedent to be false for some
        == object.

    consider blabber being PERSON such that
      1: for s being STATEMENT holds Tells[blabber,s]
                                           by BlabberMouth;         == ExE
      2': now
             assume A: Knight[blabber];
                    3: for s being STATEMENT holds 
                          Tells[blabber,s] implies True[s]
                                           by Veracity, A;           == UE, EqE
                    4: now
                        let s be STATEMENT;
                           5: Tells[blabber,s] by 1;                 == UE
                        thus True[s] by 3, 5;                        == UE, IE
                      end;
             thus for s being STATEMENT holds True[s] by 4;          == UI
         end;

      2: Knight[blabber] implies
               (for s being STATEMENT holds True[s]) by 2';          == II

    ex p being PERSON st 
        (Knight[p] implies (for s being STATEMENT holds True[s])) 
                                                    by 2;            == ExI

        == Note that we can reference 2' directly.

    ex p being PERSON st 
        (Knight[p] implies (for s being STATEMENT holds True[s])) 
                                                    by 2';           == ExI