At:
sublist transitivity111111111121111111
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.
L1: T List
9.
L2: T List
10.
L3: T List
11.
f: {T=}
12.
f TT
13.
z: T
14.
z(f) L1
15.
u: T
16.
v: T List
17.
(z:T. z(f) v z(eq) L3) z(eq) v z(eq) L3
18.
eq(z,u) = true
19.
True
20.
if f(u,u) true else u(f) v fi u(eq) L3
21.
f(u,u) u = u
22.
(f(u,u)) (u = u)
}
T
T
x:T. eq(x,x)
eq(y,x)
true
f(u,u)
