Who Cites type if?
type_if	Def A[P] == PA
	Thm* A:Type, P:Prop. A[P]  Type

Syntax:

A[P]

has structure:

type_if(A; P)

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html