At:
is member equalities lemma121111
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,y:T. f(x,y) f(y,x)
10.
x,y,z:T. f(x,y) f(y,z) f(x,z)
11.
u1: T
12.
v: T List
13.
u(eq) v u(f) v
14.
eq(u,u1) = true
15.
True
16.
eq(u,u1)
17.
u = u1
18.
f(u1,u1)
19.
f(u1,u1) = true
if f(u1,u1) true else u1(f) v fi
By:
HypSubst 19 0
THEN
Rewrite (HigherC ifthenelse_evalC THENC assert_evalC) 0
THEN
Trivial
Generated subgoals:
}
T
T
x,y:T. eq(x,y) 
x = y
if f(u1,u1)
true
