(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
(
p
:
.
q
:
.
p
q
) = (
t1
:
.
t2
:
.
t
:
.
t1
t
t2
t
t
)
By:
Simpset [`ext`] THEN Simp THEN StrongAuto
Generated subgoal:
1
1.
t1
:
2.
t2
:
(
t1
t2
) = (
t
:
.
t1
t
t2
t
t
)
5
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
(
p:
. q:. p 
q) = (t1:. t2:. 
t:. t1
tt2tt) (p:. q:. p q) = (t1:. t2:. t:. t1tt2tt)
(t1 t2) = (t:. t1tt2tt)
