(33steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
not
disjoint
is
member
lemma
1
1
1
1
1
1.
T:
Type
2.
eq:
{T=
}
3.
eq
T
T
4.
x,y:T. eq(x,y)
x = y
5.
L:
T List
6.
M:
T List
True
(
x:T. False & x(
eq) M)
By:
ListInd -1
Generated subgoals:
1
True
(
x:T. False & x(
eq) nil)
2
7.
u:
T
8.
v:
T List
9.
True
(
x:T. False & x(
eq) v)
True
(
x:T. False & x(
eq) (u.v))
About:
(33steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc