At:
sublist transitivity1111111111211211112
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.
x,y:T. f(x,y) x = y
14.
z: T
15.
z(f) L1
16.
u: T
17.
v: T List
18.
eq(z,u) = false
19.
z(eq) v
20.
z1: T
21.
z1(f) v
22.
f(z1,u) = false
23.
z1(f) v z1(eq) L3
z1(eq) L3
By:
FwdThru 23 [21]
THEN
Trivial
Generated subgoals:
}
T
T
x:T. eq(x,x)
eq(y,x)
z1(