(fix f:!x.0'+x=x'.\n:#.case n of #0 -> defP0 0'
	| v' -> (transE 0'+v' (0'+v)' v''
		{ defPS 0' v, succE 1+v  v' (f v) } )
)3