λProlog module poplmark-1a

sig poplmark-1a. kind ty type. type top ty. type arrow ty -> ty -> ty. type all ty -> (ty -> ty) -> ty. type sub, bound ty -> ty -> o.

module poplmark-1a. sub S top. sub X X :- bound X U. sub X T :- bound X U, sub U T. sub (arrow S1 S2) (arrow T1 T2) :- sub T1 S1, sub S2 T2. sub (all S1 (x\ S2 x)) (all T1 (x\ T2 x)) :- sub T1 S1, pi x\ (bound x T1 => sub (S2 x) (T2 x)).