(10steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
list
iso
iff
assert
list
iso
2
1
1.
T:
Type
2.
Discrete{T}
3.
eq:
{T
}
4.
L:
T List
5.
M:
T List
L(~eq)M
(~
eq)(L,M)
By:
Unfold `list_iso` 0
THEN
Unfold `list_iso_2` 0
THEN
Reduce 0
Generated subgoal:
1
L(
eq)M & M(
eq)L
(((
eq)(L,M))
((
eq)(M,L)))
About:
(10steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
L(
eq)M & M(eq)L 
(((
eq)(L,M))
((eq)(M,L)))
}
L(~eq)M (~eq)(L,M)
L(eq)M & M(eq)L (((eq)(L,M))((eq)(M,L)))
