%sig FOL = {
  i      : type.
  o      : type.
  forall : (i -> o) -> o.
  not    : o -> o.
  and    : o -> o -> o.         %infix none 3 and.
  =>     : o -> o -> o.         %infix none 2 =>.
  <=>    : o -> o -> o
         = [x][y]((x => y) and (y => x)).
                                %infix none 1 <=>.
  ==     : i -> i -> o.         %infix none 4 ==.
  !=     : i -> i -> o
         = [x][y] not (x == y). %infix none 4 !=.
  ded : o -> type.              %prefix 0 ded.
  
  forallI : ({x}ded A x) -> ded forall A.
  forallE : {x} ded forall A -> ded A x.
  notI    : (ded A -> ded P) -> ded not A.
  notE    : ded A -> ded not A -> ded P.
  impI    : (ded A -> ded B) -> ded (A => B).
  impE    : ded (A => B) -> ded A -> ded B.
  andI    : ded A -> ded B -> ded (A and B).
  andEl   : ded (A and B) -> ded A.
  andEr   : ded (A and B) -> ded B.
  
  eqrefl  : ded X == X.
  eqsym   : ded X == Y -> ded Y == X.
  eqtrans : ded X == Y -> ded Y == Z -> ded X == Z.
  eqcong  : ded X == Y -> ded (F X) == (F Y).
}.