types b, c
type a < b * b ->? c
ops a : a;
b : b;
c : c
. a (b, b) = c;
types
a : Type;
b : Type;
c : Type;
gn_t1[a] : +Type -> Type;
gn_t2[gn_t1[a]] : -Type -> +Type -> Type
type
gn_t2[gn_t1[a]] < __->?__
types
a := gn_t1[a] c;
gn_t1[a] := gn_t2[gn_t1[a]] (b * b)
op a : a
op b : b
op c : c
. a (b, b) = c