INDUCTIVE DEFINITION G () [ ]
OF ARITY Set
BUILT FROM:
     mk_G: Πnext:nat→nat.(∀n:nat.(lt n (next n)))→G