(4steps total) PrintForm Definitions hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ext simp 1
  'a,'b:Type, f,g:('a'b).
  (x:'a. f(x)) = (x:'a. g(x))  (x:'a. f(x) = g(x))
By: Id THEN StrongAuto

Generated subgoals:

1 1. 'a : Type
2. 'b : Type
3. f : 'a'b
4. g : 'a'b
5. (x:'a. f(x)) = (x:'a. g(x))
6. x : 'a
  f(x) = g(x)
1 step
2 1. 'a : Type
2. 'b : Type
3. f : 'a'b
4. g : 'a'b
5. x:'a. f(x) = g(x)
  (x:'a. f(x)) = (x:'a. g(x))
2 steps

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

(4steps total) PrintForm Definitions hol Sections HOLlib Doc