(4steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: trivial map
  T:Type, a:T List, f:(TT). (x:T. (x  a)  f(x) = x)  map(f;a) = a
By: Auto THEN Assert (map(f;a) = map(Id;a))

Generated subgoals:

1 1. T : Type
2. a : T List
3. f : TT
4. x:T. (x  a)  f(x) = x
  map(f;a) = map(Id;a)
2 steps
2 1. T : Type
2. a : T List
3. f : TT
4. x:T. (x  a)  f(x) = x
5. map(f;a) = map(Id;a)
  map(f;a) = a
1 step

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

(4steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc