At:
is member append lemma1122111
1.
T: Type
2.
eq: {T}
3.
eq TT
4.
x:T. eq(x,x)
5.
x,y:T. eq(x,y) eq(y,x)
6.
x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
7.
L: T List
8.
x: T
9.
u: T
10.
v: T List
11.
eq(x,u) = false
12.
x(eq) v
13.
M: T List
14.
N: T List
15.
y: T
16.
eq(x,y)
17.
v = (M @ (y.N))
M,N:T List, y:T. eq(x,y) & u.v = (M @ (y.N))
By:
Witness u.M
THEN
Witness N
THEN
Witness y
Generated subgoal:
eq(x,y) & u.v = ((u.M) @ (y.N))
}
T
T
x:T. eq(x,x)
eq(y,x)
M,N:T List, y:T. eq(x,y) & u.v = (M @ (y.N))
