At:
sublist weakening wrt identity1111111
1.
T: Type
2.
Discrete{T}
3.
eq: {T}
4.
eq TT
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.
M: T List
9.
L = M
10.
u: T
11.
v: T List
12.
eq(u,u)
13.
eq(u,u) = true
if eq(u,u) true else u(eq) v fi
By:
HypSubst -1 0
THEN
Rewrite (HigherC ifthenelse_evalC THENC assert_evalC) 0
THEN
Trivial
Generated subgoals:
}
T
T
x,y:T. eq(x,y) 
eq(y,x)
if eq(u,u)
true
