Syntax Definition ht 2

Description: The type of all functions from type al to type be.

Hypotheses

Ref	Expression
hal	type al
hbe	type be

Assertion

Ref	Expression
ht	type (al -> be)

This syntax is primitive. The first axiom using it is ax-weq 40.