% Examples: from TPTP/Proposals/HOL.html slightly modified.  -- A.V.G.
% ----------
hof(subset,definition,
    ^ [A:$type] :
    ^ [P:(A > $o),R:(A > $o)] : 
    ! [X:A] :
      ( ( P @ X )
     => ( R @ X ) )  ).

hof(set_union,definition,
    ^ [A:$type] :
    ^ [D:((A > $o) > $o),X:A] :
    ? [S:(A > $o)] :
      ( ( D @ S ) 
      & ( S @ X ) )  ).

hof(thm616A,conjecture,
    ! [A:$type] :
      ( ( ! [G:((A > $o) > $o)] :
            ( ( ( ( subset 
                  @ ( A > $o ) ) 
                @ G ) @ open ) 
           => ( open 
              @ ( ( setunion @ A ) @ G ) ) ) ) 
     => ( ! [B:(A > $o)] : 
            ( ( ! [X:A] :
                  ( ( B @ X ) 
                 => ( ? [D:(A > $o)] :
                        ( ( ( open @ D ) 
                          & ( D @ X ) ) 
                        & ( ( ( subset @ A ) @ D ) @ B ) ) ) ) ) 
           => ( open @ B ) ) ) )  ).

hof(a,conjecture,
    ! [P:(($o > $o) > $o)] :
      ( ( P @ (~) ) 
     => ( P 
        @ ^ [X:$o] : ( ~ ( ~ ( ~ X ) ) ) ) )  ).

hof(b,conjecture,
    ! [P:(($o > $o > $o) > $o)] :
      ( ( P @ (|) ) 
     => ( P 
        @ ^ [X:$o,Y:$o] :
            ( Y | X ) ) )  ).

hof(c,conjecture,
    ! [P:(($o > $o) > $o)] :
      ( ( P 
        @ ( (|) @ $true ) ) 
     => ( P 
        @ ^ [X:$o] : $true) )
  ).

hof(d,conjecture,
    ! [B:$type,A:$type] :
    ! [P:(((B > A) > (B > A) > $o) > $o)] :
      ( ( P 
        @ ( (=)
          @ ( B > A )
          )
        )
     => ( P 
        @ ^ [X:(B > A),Y:(B > A)] :
            ( Y = X )
        )
      )
  ).

hof(a,conjecture,
    ! [P:($o > $o > $o)] :
      ( ( P @ not ) 
     => ( P 
        @ ^ [X:$o] : ( not @ ( not @ ( not @ X ) ) ) ) )  ).

hof(b,conjecture,
    ! [P:(($o > $o > $o) > $o)] :
      ( ( P @ or ) 
     => ( P 
        @ ^ [X:$o,Y:$o] :
            ( or @ Y @ X ) ) )  ).

hof(c,conjecture,
    ! [P:(($o > $o) > $o)] :
      ( ( P 
        @ ( or @ $true ) ) 
     => ( P 
        @ ^ [X:$o] : $true) )  ).

hof(d,conjecture,
    ! [B:$type,A:$type] :
    ! [P:(((B > A) > (B > A) > $o) > $o)] :
      ( ( P 
        @ ( eq 
          @ ( B > A ) ) )
     => ( P 
        @ ^ [X:(B > A),Y:(B > A)] :
            ( eq @ Y @ X ) ) )  ).