(22steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
list
exists
is
member
append
lemma
1
1
1.
T:
Type
2.
P:
T
Prop
3.
L:
T List
4.
x
L.P(x)
M,N:T List, x:T. P(x) & L = (M @ (x.N))
By:
MoveToConcl -1
Generated subgoal:
1
x
L.P(x)
(
M,N:T List, x:T. P(x) & L = (M @ (x.N)))
About:
(22steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
x
L.P(x) 
(M,N:T List, x:T. P(x) & L = (M @ (x.N)))
Prop
xL.P(x)
M,N:T List, x:T. P(x) & L = (M @ (x.N))
xL.P(x) (M,N:T List, x:T. P(x) & L = (M @ (x.N)))
