(12steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
tail
1
1
1.
T:
Type
2.
Discrete{T}
3.
eq:
{T
}
4.
u:
T
5.
v:
T List
x
v.if eq(x,u)
true
else x(
eq) v fi
By:
FwdThru
Thm*
Discrete{T}
(
f:{T=
}. True) [2]
THEN
RenameVar `f' -1
Generated subgoal:
1
6.
f:
f:{T=
}. True
x
v.if eq(x,u)
true
else x(
eq) v fi
About:
(12steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
f:{T=
}. True
x
v.if eq(x,u)
true else x(eq) v fi
}
xv.if eq(x,u) true else x(eq) v fi
(f:{T=}. True)
[2]
f:{T=}. True xv.if eq(x,u) true else x(eq) v fi
