Def  Inj(A; B; f) == a1,a2:A. f(a1) = f(a2)  B  a1 = a2

is mentioned by

Thm*  n:, a,z:, s:({a...z}{1...n}Peg). Thm*  s is a Hanoi(n disk) seq on a..z Thm*   Thm*  (f:(PegPeg).  Thm*  (Inj(Peg; Peg; f)  (x,i. f(s(x,i))) is a Hanoi(n disk) seq on a..z)	[hanoi_seq_permutepegs]
Thm*  p,r,q,s:Peg. p  q  r  s  Inj(Peg; Peg; permute(p to r ; q to s))	[hanoi_peg_perm_is_inj]

In prior sections: fun 1

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html