Syntax Definition term_succ 3

Description: If '𝑡' is a term, then 's‘𝑡' is a term.

Hypothesis

Ref	Expression
term-t	term 𝑡

Assertion

Ref	Expression
term_succ	term s‘𝑡

This syntax is primitive. The first axiom using it is ax-L9-succ 22.