(13steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
iff
assert
sublist
2
T:Type. Discrete{T}
(
eq:{T
}, L,M:T List. L(
eq)M
(
eq)(L,M))
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
Discrete{T}
3.
eq:
{T
}
4.
L:
T List
5.
M:
T List
L(
eq)M
(
eq)(L,M)
About:
(13steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
}
L(
eq)M 
(eq)(L,M)
T:Type. Discrete{T} 
(eq:{T}, L,M:T List. L(eq)M (eq)(L,M))
} L(eq)M (eq)(L,M)
