(4steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
map
equal2
1
1
1.
T
: Type
2.
T'
: Type
3.
a
:
T
List
4.
f
:
T
T'
5.
g
:
T
T'
6.
x
:
T
. (
x
a
)
f
(
x
) =
g
(
x
)
7.
i
:
8.
i
<||
a
||
f
(
a
[
i
]) =
g
(
a
[
i
])
By:
BackThruSomeHyp
Generated subgoal:
1
(
a
[
i
]
a
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
T'
x:T. (x 
a) 
f(x) = g(x)
f(a[i]) = g(a[i])
