As it seems it is not possible to convert certain higher-order formulae into rewrite rules, like "forall g, x: g[x] := 0", because internally the resulting rule would look something like "g[x] := 0", which is not possible in Mathematica. The problem is that although formulae like the one above don't give an error when input into Theorema, they just don't work as rewrite rules.
On the other hand, it does work if the quantified function depends on a domain, e.g. "forall D,g,x: Poly[D][g][x] := 0" works fine.
As it seems it is not possible to convert certain higher-order formulae into rewrite rules, like "forall g, x: g[x] := 0", because internally the resulting rule would look something like "g[x] := 0", which is not possible in Mathematica. The problem is that although formulae like the one above don't give an error when input into Theorema, they just don't work as rewrite rules. On the other hand, it does work if the quantified function depends on a domain, e.g. "forall D,g,x: Poly[D][g][x] := 0" works fine.