Syntax definition wacn

Description: The axiom of choice for limited-length sequences.

	Ref	Expression
Assertion	wacn	class AC_ A