More of the THF Language

• The use of connectives as terms (THF0), e.g.,
    (& @ $false) = (^ [P:$o] : $false)

• !! and ?? for the Π (forall) and Σ (exists) operators (THF0), e.g.,
    ((!! (p)) & (!! (q))) = (! [X:$i] : ((p @ X) & (q @ X)))

• !> and ?* for Π (dependent product) and Σ (sum) types (THF), e.g.,
    cons: !> [N:nat] : ($i > (list @ N) > (list @ (succ @ N)))

• [ ] for tuples (THF), e.g.,
    make_triple = ^ [X:$i,Y:$i:,Z:$i] : [X,Y,Z]

• * and + for simple product and sum (disjoint union) types (THF), e.g.,
    roots: quadratic > (($real * $real) + $real + undef)

• := as a connective for global definitions (THFX), e.g.,
    apply_twice:= ^ [F:$o > $o,X:$o] : (F @ (F @ X))
  

• := as a separator for local definitions (ala letrec) (THFX), e.g.,
    := [NN:= (apply_twice @ ~)] : (NN = (apply_twice @ NN))

• --> as the sequent connective (THFX), e.g.,
    [p,q,r] --> [s,t]