At:
sublist functionality wrt id id list iso1121
1.
T: Type
2.
L1: T List
3.
L2: T List
4.
eq: {T}
5.
eq TT
6.
x:T. eq(x,x)
7.
x,y:T. eq(x,y) eq(y,x)
8.
x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
9.
L3: T List
10.
L4: T List
11.
Discrete{T}
12.
L1 = L2
13.
L3(eq)L4
14.
L4(eq)L3
15.
L2(eq)L4
L1(eq)L4
By:
RevHypSubst 12 15
THEN
Trivial
Generated subgoals:
}
T
T
x:T. eq(x,x)
eq(y,x)
eq)L4
L1(