(6steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose iter id 1 2
1. A : Type
2. i : 
3. 0<i
4. Id{i-1} = Id
  Id{i} = Id  AA
By: Rewrite by Thm*  f:(AA), i:. f{i} = f o f{i-1} Using:[A:= A] ...w

Generated subgoal:

1   Id o Id{i-1} = Id  AA
2 steps

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

(6steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc