% A few examples from the CAFR script

FOL : THEORY

  BEGIN

  D : TYPE+
  d : D
  P : [D -> boolean]

  D1,D2 : TYPE
  f : [D1 -> D2]
  R : [D1,D2 -> boolean]

%%

  bla : THEOREM
        (FORALL (x:D1): R(x,f(x))) IMPLIES 
          FORALL (x:D1): EXISTS (y:D2): R(x,y)

%% all these Theorems hold only classically

  exm  : THEOREM
        (FORALL (x:D): P(x)) OR (EXISTS (x:D): NOT P(x))

%% use lemma exm for depp

  depp : THEOREM
        EXISTS (x:D): FORALL (y:D): P(x) IMPLIES P(y)

%% or use contraction

  depp2 : THEOREM
        EXISTS (x:D): FORALL (y:D): P(x) IMPLIES P(y)

%% use lemma depp for doub

  doub : THEOREM
        FORALL (x,y:D): EXISTS (z:D): P(z) IMPLIES P(x) AND P(y)

%% or use contraction

  doub2 : THEOREM
        FORALL (x,y:D): EXISTS (z:D): P(z) IMPLIES P(x) AND P(y)

  END FOL