Def Trans x,y:T. E(x;y) == a,b,c:T. E(a;b)  E(b;c)  E(a;c)

is mentioned by

Thm* P:(L:(T List)(||L||-1)Prop).  Thm* Trans(T List)(_1 guarded_permutation(T;P) _2)

[guarded_permutation_transitivity]

In prior sections: rel 1 mb nat

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html