At:
list all is member lemma1122121
1.
T: Type
2.
eq: {T=}
3.
eq TT
4.
x,y:T. eq(x,y) x = y
5.
P: TProp
6.
L: T List
7.
z: T
8.
u: T
9.
v: T List
10.
xv.P(x) z(eq) v P(z)
11.
P(u)
12.
xv.P(x)
13.
if eq(z,u) true else z(eq) v fi
14.
eq(z,u)
15.
eq(z,u) = false
z(eq) v
By:
HypSubst 15 13
THEN
Rewrite (HigherC ifthenelse_evalC) 13
Generated subgoal:
1
13. z(eq) v 14. eq(z,u) 15. eq(z,u) = false z(eq) v
eq) v
eq(z,u)
z(
T
x,y:T. eq(x,y) 
x = y
true
