At:
list all all1222111
1.
T: Type
2.
eq: {T=}
3.
P: TType
4.
L: T List
5.
u: T
6.
v: T List
7.
(x:{x:T| x(eq) v }. P(x)) xv.P(x)
8.
x:{x:T| if eq(x,u) true else x(eq) v fi }. P(x)
9.
x: T
10.
x(eq) v
if eq(x,u) true else x(eq) v fi
By:
IfThenElseCases 0
Generated subgoal:
true
Type
x:{x:T| x(
eq) v }. P(x)) 
true
