At:
list iso weakening wrt identity11
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
10.
L = M
M(eq)M
By:
BackThru
Thm* Discrete{T} (eq:{T}, L,M:T List. L = M L(eq)M)
Generated subgoals:
}
T
T
x:T. eq(x,x)
eq(y,x)
M(
eq)M