(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
(
p
:
.
q
:
.
p
q
) = (
t1
:
.
t2
:
.
t
:
.
t1
t2
t
t
)
By:
Simpset [`ext`] THEN Simp THEN StrongAuto
Generated subgoal:
1
1.
t1
:
2.
t2
:
(
t1
t2
) = (
t
:
.
t1
t2
t
t
)
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
(
p:
. q:. p
q) = (t1:. t2:. 
t:. t1
t2tt) (p:. q:. pq) = (t1:. t2:. t:. t1t2tt)
(t1t2) = (t:. t1t2tt)
