(4steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rel
exp
monotone
n
:
,
T
:Type,
R1
,
R2
:(
T
T
Prop).
R1
=>
R2
R1
^
n
=>
R2
^
n
By:
InductionOnNat
Generated subgoals:
1
T
:Type,
R1
,
R2
:(
T
T
Prop).
R1
=>
R2
R1
^0 =>
R2
^0
1
step
2
1.
n
:
2. 0<
n
3.
T
:Type,
R1
,
R2
:(
T
T
Prop).
R1
=>
R2
R1
^
n
-1 =>
R2
^
n
-1
T
:Type,
R1
,
R2
:(
T
T
Prop).
R1
=>
R2
R1
^
n
=>
R2
^
n
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc