The description of why strict posivity is needed is wrong

Describe the bug
This came up on Zulip:

at the explanation for the requirements for inductive types, the example claims that the defined Fix (fun a => a -> a) would be equivalent to Bad... i've given a shot, but i couldn't seem to prove that you can construct Bad.rec function from Fix.rec? Maybe it would be easier to say that Fix (. -> Empty) is an inconsistent type (as you're creating a fixpoint for negation)?

And later in the thread:

at the explanation for the requirements for inductive types, the example claims that the defined Fix (fun a => a -> a) would be equivalent to Bad... i've given a shot, but i couldn't seem to prove that you can construct Bad.rec function from Fix.rec? Maybe it would be easier to say that Fix (. -> False) is an inconsistent type (as you're creating a fixpoint for negation)?

I looked into this and indeed Lean generates a recursor without an induction hypothesis for Fix.rec:

unsafe inductive Fix (f : Type u → Type u) where
  | fix : f (Fix f) → Fix f

#check Fix.rec
-- Fix.rec.{u_1, u} {f : Type u → Type u} {motive : Fix f → Sort u_1}
--   (fix : (a : f (Fix f)) → motive (Fix.fix a))
--   (t : Fix f) : motive t

So I guess the Fix that comes out of the unsafe inductive declaration is an accidentally consistent but non-inductive type.

And the the answer:

it's still not consistent, using f := (. -> Empty)

my point is that the argument as to why it isn't consistent is wrong (or at least not clear)

This should be investigated and fixed.

Open the linked Well-formed inductives section and compare the Fix (fun a => a -> a) explanation with the Zulip discussion, especially Fix.rec and the f := (. -> Empty) case. Clarify the consistency argument in the documentation and verify the revised explanation against the surrounding requirements text; no specific test is named.