; Simple Type Theory as a theory in predicate logic.
;
; Use reverse polish notation for names, eg:
;   * i -> i becomes iia,
;   * i -> i -> i becomes iiiaa
;   * (i -> i) -> i becomes iiaia

o : Type.
eps : o -> Type.

i : Type.
iia : Type.
iiiaa : Type.
iiiiaaa : Type.
iiaia : Type.
iiiaaiiaiiaaa : Type.
iiaiiaa : Type.

ooa : Type.
oooaa : Type.
ioaoa : Type.
iiaoaoa : Type.
iiiaaoaoa : Type.

O : i.
S : iia.

ap_iia : iia -> i -> i.
ap_iiiaa : iiiaa -> i -> iia.
ap_iiiaaiiaiiaaa : iiiaaiiaiiaaa -> iiiaa -> iiaiiaa.
ap_iiaiiaa : iiaiiaa -> iia -> iia.

ap_ooa : ooa -> o -> o.
ap_oooaa : oooaa -> o -> ooa.

one : i.
[] one --> ap_iia S O.

imp : oooaa.
forall_i : ioaoa.
forall_iia : iiaoaoa.
forall_iiiaa : iiiaaoaoa.

; S and K combinators.
S_iiiaaiiaiiaaa : iiiaaiiaiiaaa.
K_iiiaa : iiiaa.

[ x : iiiaa
, y : iia
, z : i ]
ap_iia (ap_iiaiiaa (ap_iiiaaiiaiiaaa S_iiiaaiiaiiaaa x) y) z --> ap_iia (ap_iiiaa x z) (ap_iia y z).
[ x : i
, y : i ]
ap_iia (ap_iiiaa K_iiiaa x) y --> x.
[ x : o
, y : o ]
eps (ap_ooa (ap_oooaa imp x) y) --> eps x -> eps y.