(5steps total)
PrintForm
Definitions
Lemmas
hol
sum
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hrep
sum
inj
'a
,
'b
:S,
u
,
v
:
'a
+
'b
. rep_sum(
u
) = rep_sum(
v
)
'a
'b
u
=
v
By:
Id THEN StrongAuto
Generated subgoal:
1
1.
'a
: S
2.
'b
: S
3.
u
:
'a
+
'b
4.
v
:
'a
+
'b
5. rep_sum(
u
) = rep_sum(
v
)
'a
'b
u
=
v
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
Lemmas
hol
sum
Sections
HOLlib
Doc
'a,'b:S, u,v:'a+'b. rep_sum(u) = rep_sum(v) 
'a'b 
u = v 'a,'b:S, u,v:'a+'b. rep_sum(u) = rep_sum(v) 'a'b u = v 'a'b
u = v
