Nuprl - Proof: reduce wf 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: reduce wf 1 2 1

1. A : Type
2. B : Type
3. f : A

B
4. k : B
5. A List
6. u : A
7. v : A List
8. reduce(f;k;v)

f(u,reduce(f;k;v))

By:

Analyze

Generated subgoals:

1 f(u) BB
Auto

2 reduce(f;k;v) B
Trivial

About:

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