Nuprl - Proof: ext simp 2

(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 2

'a,'b:Type, f,g:('a

'b). f = (

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. f = (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)
f = (x:'a. g(x))
2 steps

About:

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

(4steps total) PrintForm Definitions hol Sections HOLlib Doc

1	1. 'a : Type 2. 'b : Type 3. f : 'a'b 4. g : 'a'b 5. f = (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) f = (x:'a. g(x))	2 steps