fix f:!a.!b.a+b=b+a.
	\x:#.\n:#.case n of #0 -> 
		(transE x+0 x 0+x {defP0 x, symmE 0+x x (thm0P x)} )
	| v' -> 
	  (transE8
		 x+v'
		(x+v)'
		(v+x)'
		 v+x'
		 v+(0'+x)
		(v+0')+x
		(v+0)'+x
		 v'+x

		{ defPS  x  v
		, succE  x+v  v+x  (f x v)
		, symmE  v+x' (v+x)' (defPS v x)
		, thmPE  v  x'  0'+x (symmE 0'+x  x' (thm1P x))
		, symmE (v+0')+x  v+(0'+x) (assocP v 0' x)
		, thmPE2  x  v+0' (v+0)' (defPS v 0)
		, thmPE2  x (v+0)' v' (succE v+0 v (defP0 v))
		}
	)