(4steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: reverse append
  T:Type, as,bs:T List. rev(as @ bs) = (rev(bs) @ rev(as))
By: (CDToVarThen `as' ListInd) THEN (Reduce 0)

Generated subgoals:

1 1. T : Type
2. T List
  bs:T List. rev(bs) = (rev(bs) @ nil)
1 step
2 1. T : Type
2. T List
3. u : T
4. v : T List
5. bs:T List. rev(v @ bs) = (rev(bs) @ rev(v))
  bs:T List. (rev(v @ bs) @ [u]) = (rev(bs) @ rev(v) @ [u])
2 steps

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

(4steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc