(26steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
list
all
all
1
1.
T:
Type
2.
eq:
{T=
}
3.
P:
T
Type
4.
L:
T List
x
L.P(x)
(
x:{x:T| x(
eq) L }. P(x))
By:
Analyze 0
Generated subgoals:
1
5.
x
L.P(x)
6.
x:
{x:T| x(
eq) L }
P(x)
2
5.
x:{x:T| x(
eq) L }. P(x)
x
L.P(x)
About:
(26steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
x
L.P(x)eq) L }
P(x)x:{x:T| x(eq) L }. P(x) xL.P(x)
}
Type
xL.P(x) 
(x:{x:T| x(eq) L }. P(x))
xL.P(x)eq) L } P(x)x:{x:T| x(eq) L }. P(x) xL.P(x)
