'a:S, h:'a, t:'a List, h':'a, t':'a List.
  cons(h; t) = cons(h'; t')  h = h' & t = t'

By:	Auto THEN LemmaRW Thm* 'a:S, h:'a, t:'a List, h':'a, t':'a List. Thm* cons(h; t) = cons(h'; t')  h = h' & t = t'

None

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