PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fappend
wf
n
,
m
:
,
f
:(
n
m
),
x
:
m
.
f
[
n
:=
x
]
(
n
+1)
m
By:
Auto THEN Unfold `fappend` 0 THEN Analyze THEN SplitOnConclITE
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
n,m:
, f:(n
m), x:m. f[n:=x] 
(n+1)m n,m:, f:(nm), x:m. f[n:=x] (n+1)m
