Nuprl - Proof: compose iter prod2

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

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

A), i,j:

. f{

i}{

j}(x) = f{

j}(x)

By:	SimilarTo: Thm* x:A, f:(AA), i,j,k:. k = ij f{i}{j}(x) = f{k}(x) A ...

Generated subgoal:

1 1. A : Type
2. x : A
3. f : AA
4. i :
5. j :
6. k:. k = ij f{i}{j}(x) = f{k}(x)
f{i}{j}(x) = f{ij}(x)
1 step

About:

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