tv - Higher-Order Logic Explorer

	Higher-Order Logic Explorer		< Wrap Next > Nearby theorems
Mirrors > Home > HOLE Home > Th. List > tv		GIF version

Syntax Definition tv 1

Description: A var is a term.

**Hypotheses**
Ref	Expression
hal	type α
vx	var x

**Assertion**
Ref	Expression
tv	term x:α

This syntax is primitive. The first axiom using it is ax-cb1 29.

Colors of variables: type var term