doc: fix incorrect subsingleton criteria

[ia0]

This PR fixes 2 aspects of the subsingleton criteria:

• It's not the constructor parameter type which must be a parameter or index. It's the parameter itself. That's demonstrated by Eq.
• A constructor parameter doesn't need to be a proof or a parameter/index, it can also be recursive. That's demonstrated by Acc. This example has been added to the list of examples, in addition to the criteria fix.

I'm happy to reword the criteria and example. Note that I used the word "argument" to mean both "parameter" and "index" as is done previously in the reference manual:

reference-manual/Manual/Language/InductiveTypes.lean

Line 87 in c8193e0

Type constructors may take two kinds of arguments: {deftech}_parameters_ {index (subterm := "of inductive type")}[parameter] and {deftech (key := "index")}_indices_.{index (subterm := "of inductive type")}[index]

Here is a more formal description of the criteria:
https://github.com/digama0/lean-type-theory/blob/0ba178704380d2fad751f020d461b293f47e36d5/axioms.tex#L148

[github-actions]

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 17c04bb.