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

By:	Auto THEN Unfolds [`guarded_permutation`;`trans`] 0 THEN Reduce 0 THEN Using [`y',b] (BackThru (Thm* R:(TTProp), x,y,z:T. (x (R^*) y)  (y (R^*) z)  (x (R^*) z))

None

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