Nuprl - Proof: compose iter id 1 2 1

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

1. A : Type
2. i :

3. 0<i
4. Id{

i-1} = Id

Id o Id{

i-1} = Id

By:	Rewrite by Thm* f:(AB). Id o f = f AB Using:[A:= A \| B:= A] ...w

Generated subgoal:

1 Id{i-1} = Id AA
Hypothesis

About:

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