Nuprl - Proof: compose iter prod

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

A:Type, x:A, f:(A

A), i,j,k:

. k = i

i}{

j}(x) = f{

k}(x)

By:	Guarding (j:. <prop>) Auto THEN CompNatInd Concl

Generated subgoal:

1 1. A : Type
2. x : A
3. f : AA
4. i :
5. j :
6. j1:. j1<j (k:. k = ij1 f{i}{j1}(x) = f{k}(x))
7. k :
8. k = ij
f{i}{j}(x) = f{k}(x)
13 steps

About:

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