Definition wat 180

Description: The type of the indefinite descriptor.

Assertion

Ref	Expression
wat	|- @:((al -> *) -> al)

Detailed syntax breakdown of Definition wat

Step	Hyp	Ref	Expression
1		hal	. . . 4 type al
2		hb 3	. . . 4 type *
3	1, 2	ht 2	. . 3 type (al -> *)
4	3, 1	ht 2	. 2 type ((al -> *) -> al)
5		tat 179	. 2 term @
6	4, 5	wffMMJ2t 12	1 wff @:((al -> *) -> al)

This definition is referenced by:  ac  184  dfex2  185  exmid  186