ch:subject-dependent-self: subject-dependent self

From $t:T[t/x]$, S-Self-Gen yields $t:\iota x.T$; then S-Self-Inst yields $t:T[t/x]$ again. Both steps retain the Curry subject, so every erasure is $\mathrm{erase}(t)$. The instantiation rule substitutes the subject actually classified, namely $t$. It supplies neither a conversion with $T[u/x]$ nor an equality $t=u$, so no equation involving an unrelated $u$ follows.

In context $A:{\mathcal{U}}_0$, the nil constructor has type $\mathsf{Vec}(A,\mathsf{0})$ and erases to $\lambda z.\lambda s.z$. Indeed, for $$C:\prod _{k:\mathsf{Nat}}\mathsf{Vec}(A,k)\to {\mathcal{U}}_0,z:C(\mathsf{0},\mathsf{vnil}),$$ it returns $z$.

For $k:\mathsf{Nat}$, $a:A$, and $xs:\mathsf{Vec}(A,k)$, the cons constructor has type $\mathsf{Vec}(A,\mathsf{S}(k))$ and erases to $$\lambda z.\lambda s.skaxs(xszs).$$ Self instantiation at $xs$ gives $xszs:C(k,xs)$, so the step premise gives $$skaxs(xszs):C(\mathsf{S}(k),\mathsf{vcons}(k,a,xs)).$$ Rule S-Self-Gen closes both constructor typings.

Finally fix $n:\mathsf{Nat}$ and $v:\mathsf{Vec}(A,n)$. Rule S-Self-Inst substitutes the classified subject $v$ for the self variable and yields $vzs:C(n,v)$. Abstracting over $v$ and then $n$ gives $$\prod _{n:\mathsf{Nat}}\prod _{v:\mathsf{Vec}(A,n)}C(n,v).$$ The binder $n$ is explicit in the context and in the result; no free length variable remains. Erasure is the ordinary Church-vector fold.

Fix $C,s,z,n$. From $n:\mathsf{Nat}$, S-Self-Inst gives $$n:\mathrm{\forall }C.(\mathrm{\forall }k.C(k)\to C(Sk))\to C(0)\to C(n).$$ Implicit elimination at $C$, then application to $s$ and $z$, yields $nsz:C(n)$. The occurrence of $n$ in this result is exactly the subject substituted by self instantiation. Abstracting supplies the theorem’s type. If $C$ is constant at $D$, the erasure is $\lambda s.\lambda z.\lambda n.nsz:(D\to D)\to D\to D$, the Church iterator.

In $1+X\times X$, both occurrences are positive, so the closure admits it. In $X\to \mathsf{N}$, the occurrence is in an arrow domain and is negative, so it is rejected. In $(X\to \mathsf{N})\to \mathsf{N}$, the two domain crossings restore positive polarity, so it is admitted. For the rejected body, candidate monotonicity would require $R\subseteq S\Rightarrow (R\Rightarrow N)\subseteq (S\Rightarrow N)$. Function-space variance gives the reverse inclusion instead, so the fixed point construction cannot use it as a monotone operator.