(5steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hand
def
1
1
1.
t1
:
2.
t2
:
(
t1
t2
) = (
t
:
.
t1
t2
t
t
)
By:
Simpset [`bequal`] THEN Simp THEN StrongAuto THEN HypBackchain THEN Simp
THEN
StrongAuto
Generated subgoals:
1
3.
t
:
. (
t1
t2
t
)
t
t1
1
step
2
3.
t
:
. (
t1
t2
t
)
t
t2
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
(t1
t2) = (
t:. t1
t2tt)
(t1t2) = (t:. t1t2tt)t:. (t1 t2 t) t
t1
t:. (t1 t2 t) t
t2
