At:
list iso inversion
1
1
1.
T: Type
2.
Discrete{T}
3.
eq1: {T
}
4.
eq1 
T
T
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(~eq1)L
By:
UnfoldTopAb -1
THEN
Analyze -1
THEN
UnfoldTopAb 0
THEN
Analyze 0
THEN
Trivial
Generated subgoals:
None
About:
