(10steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
list
iso
iff
assert
list
iso
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:
(10steps)
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)
