(10steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

At: list iso iff assert list iso 2 1 1 1

1. T: Type
2. Discrete{T}
3. eq: {T}
4. eq TT
5. x:T. eq(x,x)
6. x,y:T. eq(x,y) eq(y,x)
7. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
8. L: T List
9. M: T List

L(eq)M & M(eq)L (eq)(L,M) & (eq)(M,L)

By:
Analyze 0
THEN
Analyze 0


Generated subgoals:

110. L(eq)M & M(eq)L
(eq)(L,M) & (eq)(M,L)
210. (eq)(L,M) & (eq)(M,L)
L(eq)M & M(eq)L

About:
listboolassertapplyfunctionuniversememberimpliesandall

(10steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc