(35steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
list
exists
append
lemma
2
2
1
1
1.
T:
Type
2.
P:
T
Prop
3.
M:
T List
4.
u:
T
5.
v:
T List
6.
L:T List.
x
L.P(x)
x
v.P(x)
x
(L @ v).P(x)
7.
L:
T List
False
P(u)
x
v.P(x)
P(u)
x
v.P(x)
By:
Auto
Generated subgoal:
1
8.
False
P(u)
x
v.P(x)
P(u)
x
v.P(x)
About:
(35steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
P(u) 
x
v.P(x)
P(u) xv.P(x)
Prop
L:T List. xL.P(x) xv.P(x) 
x(L @ v).P(x)
False P(u) xv.P(x) P(u) xv.P(x)
P(u) xv.P(x) P(u) xv.P(x)
