Nuprl - Proof: hone one def 1

(4steps total) PrintForm Definitions hol bool Sections HOLlib Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hone one def 1

1. 'b : S
2. 'a : S
3. f : 'a

(

one_one('a;'b;f)) = (

x1,x2:'a. ((f(x1)) =

(f(x2)))

(x1 =

x2))

By:	Unab [`one_one`] THEN Simpset [`bequal`] THEN Simp THEN StrongAuto

Generated subgoals:

1 4. x,y:'a. f(x) = f(y)  x = y
5. x1 : 'a
6. x2 : 'a
7. f(x1) = f(x2)
  x1 = x2
1 step

2 4. x1,x2:'a. f(x1) = f(x2)  x1 = x2
5. x : 'a
6. y : 'a
7. f(x) = f(y)
  x = y
1 step

About:

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

(4steps total) PrintForm Definitions hol bool Sections HOLlib Doc

1	4. x,y:'a. f(x) = f(y) x = y 5. x1 : 'a 6. x2 : 'a 7. f(x1) = f(x2) x1 = x2	1 step
2	4. x1,x2:'a. f(x1) = f(x2) x1 = x2 5. x : 'a 6. y : 'a 7. f(x) = f(y) x = y	1 step