(16steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
is
member
of
append
lemma
1
1.
T:
Type
2.
eq:
{T
}
3.
L:
T List
4.
M:
T List
5.
x:
T
x(
eq) (L @ M)
x(
eq) L
x(
eq) M
By:
Analyze 0
THEN
Analyze 0
Generated subgoals:
1
6.
x(
eq) (L @ M)
x(
eq) L
x(
eq) M
2
6.
x(
eq) L
x(
eq) M
x(
eq) (L @ M)
About:
(16steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
eq) (L @ M)
x(eq) L 
x(eq) Meq) L x(eq) M x(eq) (L @ M)
}
x(eq) (L @ M) 
x(eq) L x(eq) M
eq) (L @ M) x(eq) L x(eq) Meq) L x(eq) M x(eq) (L @ M)
