Nuprl - Proof: compose iter injection2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose iter injection2 2

1. A : Type
2. f : A inj

A
3. Inj(A; A; f)

(

. Inj(A; A; f{

i}))
4. i :

A inj

By:

Analyze-3

Generated subgoal:

1 2. f : AA
3. Inj(A; A; f)
4. Inj(A; A; f) (i:. Inj(A; A; f{i}))
5. i :
f{i} A inj A
2 steps

About:

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