(9steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
remove
wf
1
1.
T:
Type
2.
eq:
T
T
3.
x:
T
4.
L:
T List
remove(eq;x;L)
T List
By:
ListInd 4
Generated subgoals:
1
remove(eq;x;nil)
T List
2
5.
u:
T
6.
v:
T List
7.
remove(eq;x;v)
T List
remove(eq;x;(u.v))
T List
About:
(9steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
remove(eq;x;nil) 
T List T List remove(eq;x;(u.v)) T List
T
remove(eq;x;L) T List
remove(eq;x;nil) T List T List remove(eq;x;(u.v)) T List
