enrich
nat-basic,
elem
with
constants
aa : Elem;
predicates
ok : Elem;
rel : Elem × Elem;
variables
nf : Nat → Elem;
nfgen : Nat → Nat → Elem;
elemf : Elem → Elem;
a : Elem;
b : Elem;
c : Elem;
m : Nat;
n : Nat;
end enrich