Nuprl - Proof: compose iter injection2

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

A:Type, f:(A inj

A), i:

. f{

A inj

By:	SimilarTo Thm* Inj(A; A; f) (i:. Inj(A; A; f{i}))

Generated subgoals:

1 1. A : Type
2. f : A inj A
  f  AA
1 step

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

About:

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

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