Nuprl - Proof: injtype vs inj 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: injtype vs inj 1

1. A : Type
2. B : Type

(

{f:(A

B)| Inj(A; B; f) })

(

f:(A

B). Inj(A; B; f))

By:

Analyze

Generated subgoals:

1 3. {f:(AB)| Inj(A; B; f) }
f:(AB). Inj(A; B; f)
2 steps

2 3. f:(AB). Inj(A; B; f)
{f:(AB)| Inj(A; B; f) }
1 step

About:

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

1	3. {f:(AB)\| Inj(A; B; f) } f:(AB). Inj(A; B; f)	2 steps
2	3. f:(AB). Inj(A; B; f) {f:(AB)\| Inj(A; B; f) }	1 step