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

At: list iso inversion 1
1. T: Type
2. Discrete{T}
3. eq1: {T}
4. eq1 TT
5. x:T. eq1(x,x)
6. x,y:T. eq1(x,y) eq1(y,x)
7. x,y,z:T. eq1(x,y) eq1(y,z) eq1(x,z)
8. eq2: {T}
9. eq2 TT
10. x:T. eq2(x,x)
11. x,y:T. eq2(x,y) eq2(y,x)
12. x,y,z:T. eq2(x,y) eq2(y,z) eq2(x,z)
13. L: T List
14. M: T List
15. eq1 = eq2 {T}
16. L(~eq1)M

M(~eq2)L
By: RevHypSubst 15 0 THENA Equivalence -1
Generated subgoal:

1 M(~eq1)L

About:
listboolassertapplyfunctionuniverseequalmemberimpliesall

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