(2steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
decidable
is
member
T:Type, eq:(T
T
), x:T, L:T List. Dec(x(
eq) L)
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
eq:
T
T
3.
x:
T
4.
L:
T List
Dec(x(
eq) L)
About:
(2steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc