λProlog module
type-uniq
type-uniq.sig
sig type-uniq. kind tm, ty type. type app tm -> tm -> tm. type abs ty -> (tm -> tm) -> tm. type arrow ty -> ty -> ty. type of tm -> ty -> o.
type-uniq.mod
module type-uniq. of (abs T R) (arrow T U) :- pi x\ (of x T => of (R x) U). of (app M N) T :- of M (arrow U T), of N U.
