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