(10steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
sq
stable
is
member
1
1.
T:
Type
2.
eq:
T
T
3.
x:
T
4.
L:
T List
SqStable(x(
eq) L)
By:
ListInd 4
Generated subgoals:
1
SqStable(x(
eq) nil)
2
5.
u:
T
6.
v:
T List
7.
SqStable(x(
eq) v)
SqStable(x(
eq) (u.v))
About:
(10steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
SqStable(x(
eq) nil)eq) v) SqStable(x(eq) (u.v))
T
SqStable(x(eq) L)
SqStable(x(eq) nil)eq) v) SqStable(x(eq) (u.v))
