(9steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
non
nil
is
member
1
1.
T:
Type
2.
eq:
{T
}
3.
eq
T
T
4.
x:T. eq(x,x)
5.
x,y:T. eq(x,y)
eq(y,x)
6.
x,y,z:T. eq(x,y)
eq(y,z)
eq(x,z)
7.
L:
T List
8.
L
nil
x:T. x(
eq) L
By:
ListInd 7
Generated subgoals:
1
nil
nil
T List
(
x:T. x(
eq) nil)
2
8.
u:
T
9.
v:
T List
10.
v
nil
(
x:T. x(
eq) v)
u.v
nil
(
x:T. x(
eq) (u.v))
About:
(9steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc