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