ChainRelation: <*>
ApFun: <fun> to: <arg>
CoerceToType <term> <ml>
TypeTagging[num]: <*>

At Type{[level]} <ml>

Repeat <ml>
[num] Times <ml>

Analyze'[clause]
Witness[clause]: <terms>
Select[clause]:  1 |2
FunExtensionality

<terms>  Asserted Enough: <terms>
<terms>  By <ml> Decide: <terms>
DescribeFun: <var> by <!>

SimilarTo: <*>
BackThru: <*>
FwdThru: <*> on [ <terms> ]
Inst: <*>
<ml> Using:{<levels>}[<terms>]

Rewrite[clause] by <*>
Subst[clause]: <*>

New:<vars> <ml>
Rename[num]: <var>
CBV[num]: <term>

<ml> {Auto'} <ml> {Id}
<ml> {TryComplete Auto}
<ml> {Auto sans <pattern>}
<ml>  <hyp>

<term>
Tms:[<terms>]
subst:{<levels>}[<terms>]
RuleArgs:[<terms>]

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