Syntax definition c2ndf

Description: Extend class notation with the second projection functor.

	Ref	Expression
Assertion	c2ndf	$$class{2^{nd}}_F$$