At:
is member equalities lemma122
1.
T: Type
2.
eq: {T=}
3.
eq TT
4.
x,y:T. eq(x,y) x = y
5.
u: T
6.
L: T List
7.
f: {T}
8.
f TT
9.
x:T. f(x,x)
10.
x,y:T. f(x,y) f(y,x)
11.
x,y,z:T. f(x,y) f(y,z) f(x,z)
12.
u1: T
13.
v: T List
14.
u(eq) v u(f) v
15.
eq(u,u1) = false
16.
u(eq) v
if f(u,u1) true else u(f) v fi
By:
GenConcl (f(u,u1) = b)
THEN
BoolInd -2
THEN
Rewrite (HigherC ifthenelse_evalC THENC TryC (HigherC assert_evalC)) 0
THEN
Try Trivial
Generated subgoal:
u(
f) v
T
x,y:T. eq(x,y) 
x = y
true
