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