\w:(P(0)&(!n.P(n)->P(n'))).
	fix f:!m.P(m).
	\k:#.case k of #0 -> (proj 1 w)
		| v' -> ((proj 2 w) v (f v))