(3steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: concat append
  ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2))
By: InductionOnList THEN Unfold `concat` 0 THEN Reduce 0 THEN Fold `concat` 0
THEN
UnivCD

Generated subgoals:

1 1. (Top List) List
2. ll2 : (Top List) List
  concat(ll2) ~ concat(ll2)
Auto
2 1. (Top List) List
2. u : Top List
3. v : (Top List) List
4. ll2:(Top List) List. concat(v @ ll2) ~ (concat(v) @ concat(ll2))
5. ll2 : (Top List) List
  (u @ concat(v @ ll2)) ~ ((u @ concat(v)) @ concat(ll2))
1 step

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

(3steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc