Nuprl Basics - Proof: sfa doc type poly swap 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc type poly swap 1 1

1. f :

C,D:Type. C

C
2. A : Type
3. B : Type
4. a : A
5. b : B
6. f

{a:A}

{b:B}

{a:A}

f(<a,b>) = <b,a>

By:	BackThru: z:({b:B}{a:A}). z = <b,a> BA

Generated subgoals:

1 7. z : {b:B}{a:A}
  z = <b,a>  BA
4 steps

2   a  {a:A}
1 step

3   b  {b:B}
1 step

About:

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